Aseem Rastogi

The following fails, if we uncomment `assert_spinoff` then it succeeds. The reason is that `pts_to` gets reduced to `Mk_vprop` with lambdas as arguments, that end up getting different smt encoding:...

A formula like `forall x1. forall. x2. exists x3. phi` gets resugared to, and hence pretty printed as, `forall x1 x2 x3. phi`. The bug is in the `uncurry` function...

@john-ml reports the following failing code: ``` noeq type fn a b = { f: a -> b } let extract_left #a #b : fn (x:either a b{Inl? x}) a...

Notes from a meeting between @fournet, @ad-l, and @aseemr: We will work towards an implementation of HS ans HSL consisting of both low-level and high-level components. On the reading side,...

Cleanup of compiler hacking subp-prover args in fstar-mode.el

6

Hi Clement: I recently added support for typechecking the F* typechecker source files in the emacs mode via Makefile(s) and the `-in` targets. This helps keep the F* command line...

See https://github.com/FStarLang/fstar-mode.el/issues/113.

Imprecise logical context in the match branch (cannot prove that the scrutinee is not a data constructor that is matched before this branch)

1

``` noeq type t = | A : t | B : t fn test (x:t) requires emp ensures emp { match x { A -> { () } _...

Meta issue for syntax improvements in Pulse

1

- [x] `fn (p:int -> int) ...` doesn't parse, it has to be written as `fn (p:(int -> int)) ...` (note the extra parenthesis around the arrow) - [x] `let...

More of an F* issue, but since the main client of F* reflection typing is Pulse, and the F* change would require some churn in the Pulse checker, making an...

The typing rules in Pulse and Reflection were written when we did not have substitutions as first class entities. As a result, rules often say `open (close c x) e`...