FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
Hello! I just found this very helpful property has its `SMTPat` commented out: https://github.com/fstarlang/FStar/blob/master/ulib/FStar.List.Tot.Properties.fst#L191-L199 ```fstar val append_mem: #t:eqtype -> l1:list t -> l2:list t -> a:t -> Lemma (requires True)...
Hi, checking out the latest pre-release in the repo: https://github.com/fstarlang/fstar/releases I downloaded the Darwin archive and extracted it, then went into `bin/` and found the binary is named `fstar.exe`. Using...
The attached file shows this bug on the last definition (which was under construction), print_implicits/universes was on but provided no help. (Error 19) Subtyping check failed; expected type p’: pfp...
Folks, A Seq length = n constraint in a conjunctive refinement type is order dependent. (* This demonstrates a type checking problem in which a sequence is used before it's...
This adds `_unsafe` versions for modulo, shift left and shift right.
type listset' (e: eqtype) = list e let rec lsmem #e (e': e) (ls: listset' e) : Tot bool = match ls with | [] -> false | hd::tl ->...
```fstar module Unk open FStar.Tactics.V2 let must_check (g:env) (e:term) (ty:term) : Tac (typing_token g e (E_Total, ty)) = match core_check_term g e ty E_Total with | Some tok, _ ->...
``` $ cat ZZ.fst module ZZ friend IDontExist $ cat ZZ.fsti module ZZ $ fstar.exe ZZ.fst ZZ.fst(3,0-3,17): (Error 310) 'friend' declarations cannot refer to modules that lack interfaces 1 error...
This allows to user a witnessed token in recursive definitions in non-strictly positive positions. The justification is 1) that this token is really just a unit, it's the axiom that...
The range info on these constructs is set to dummyRange. Discovered by @bollu .. thanks!
