The Pulse parser no longer has special treatment for vprops. So, this also gets rid of the `@ syntax of embedding F terms inside Pulse vprop, since the syntax of a Pulse vprop is now just the syntax of F terms.
This fixes a couple of open issues: #50 #14 (and gets rid of some WHY WHY WHY remarks in Tahina's Pulse code).
The syntax of vprops in Pulse now coincides with their syntax in F*.
The main enabler was the addition of overloaded quantifier tokens in F*, i.e., https://github.com/FStarLang/FStar/pull/3149
Now, you can write
for vprops in both F* and Pulse contexts.
The Pulse parser no longer has special treatment for vprops. So, this also gets rid of the `@ syntax of embedding F terms inside Pulse vprop, since the syntax of a Pulse vprop is now just the syntax of F terms.
This fixes a couple of open issues: #50 #14 (and gets rid of some WHY WHY WHY remarks in Tahina's Pulse code).