Argument to bi_pure should have argument at type_scope?
The argument of bi_pure
is marked as stdpp
scope, which seems odd since it is a Prop
? This works since all notations inside of stdpp have stdpp_scope, but it isn't nicely compatible with non stdpp notations.
If you already have a Open Scope stdpp_scope
in your file, you should already get access to notations in stdpp scope.