nikswamy

Part of what added to my confusion was that if you do: ``` fn test_elim_pure (x:option bool) requires exists* q. q ** pure (Some? x) ensures emp { show_proof_state(); let...

@mtzguido has added support for general recursion in `stt` as well as recursion with termination checking for `stt_ghost`. We also have support for extraction of recursive definitions. The approach involves...

The trouble with record literal syntax and unary transform is addressed here: https://github.com/FStarLang/steel/commit/7b877db686390522314945e6ffb092602aed04fc

This now fails with a localized error on `spawn (pth n)`, saying "Elaborated term has unresolved implicits". If you turn on print_implicits and print_universes you see ``` Bug45.spawn u#_ u#_...

This program fails to check blaming the entire program, instead of just the equality of a == c * y. ```pulse fn multiply_by_repeated_addition (x y:nat) requires emp returns z:nat ensures...

Fixed in 5c18b713a891323d828a5591fd6e2c7c4f00af16

I have a fix to at least the main symptom reported in this issue. However, keep in mind that the Pulse unifier is, by design, very simple, e.g., it does...