Guido Martínez
Guido Martínez
- Mutable parameters - A rudimentary testsuite - A README.md - Some more basic static checks (that cause an assertion failure when not met)
This PR fixes spurious uses of names, as described in FStarLang/FStar#1905. F* will reject these names with a syntax error once the fix is merged (waiting on this PR and...
This PR fixes spurious uses of names, as described in FStarLang/FStar#1905. F* will reject these names with a syntax error once the fix is merged (waiting on this PR and...
When FStarLang/FStar#2730 is merged, `term_eq` will have some slight differences in behavior. In particular it will not ignore universes any more so I believe most calls here will fail. Since...
Discussed with @nikswamy today: always loading the definitions for all tuples (normal ones up to 14, dependent up to 5) is an unnecessary load on the typechecker and SMT solver....
``` $ cat AA.fst module Aa ``` ``` $ cat BB.fst module BB open AA ``` Trying to check `BB` gives: ``` $ ./bin/fstar.exe BB.fst * Warning 241 at AA.fst(0,0-0,0):...
Currently, we consider that the value for a machine integer (say U32) is a term of the form `FStar.UInt32.uint_to_t 42`, or potentially `UInt32.__uint_to_t 42`, and rely as well on some...
```fstar module VerifiedTransform open FStar.Tactics.V2 open FStar.Reflection.Typing let t_unit = `() let mk_eq2 (ty t1 t2 : term) : Tot term = (`squash (eq2 #(`#ty) (`#t1) (`#t2))) let valid (g:env)...
```fstar module P open FStar.Tactics.V2 #push-options "--lax" let aux2 (p:Type0) : Lemma True = calc (==>) { squash p; ==> { _ by (apply (`Squash.join_squash); hyp (nth_var (-1))) } p;...