After some fixes in F* (FStarLang/FStar#3329) this now works more reliably.
There is one giant problem still, which is that the check for all vals being defined is done during interleaving, and at that time there are no vals for the Pulse definitions (they are just syntax extension blobs) so we never report an error if we forgot to define something (or made a typo in the name). I think we can fix this in F* by keeping track of yet-undefined vals in the typechecker. Fixed by https://github.com/FStarLang/FStar/pull/3330
Also, the syntax blobs don't really have a name, so they do not get interleaved properly.
After some fixes in F* (FStarLang/FStar#3329) this now works more reliably.
There is one giant problem still, which is that the check for all vals being defined is done during interleaving, and at that time there are no vals for the Pulse definitions (they are just syntax extension blobs) so we never report an error if we forgot to define something (or made a typo in the name). I think we can fix this in F* by keeping track of yet-undefined vals in the typechecker.Fixed by https://github.com/FStarLang/FStar/pull/3330Also, the syntax blobs don't really have a name, so they do not get interleaved properly.