⌜...⌝ uses bad scopes
⌜x = y + z⌝
shows a really strange error: it complains that y
is expected to have type Type
.
The reason is here:
Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
This leads to +
being interpreted as a type.
I think we should remove %type
here. Not sure about %stdpp
.