FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
```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;...
This tripped me in Pulse examples where the directory is `_output/cache`, and set in the extension config, so the extension would not start. ``` $ fstar.exe --cache_dir d1 # OK...
```f* module Bug open FStar.Tactics.Effect let crash () : Tac int = let rec aux () : Tac int = 123 in let r = aux () in r ```...
This works just fine, even if the lemma works on squashes (or on just pp/qq) ```fstar assume val pp : prop assume val qq : prop assume val ii :...
```fstar unfold let maybe_ghost (b:bool) (post : unit -> prop) = if b then unit -> squash (post ()) else unit -> squash (post ()) noeq type r (p:Type) =...
This is not ready and CI will fail, but posting it here to keep track that we should probably do this eventually. The current errors I see are: ``` *...
This crashes with "antiquotation out of bounds". Removing the open also causes a (hopefully silly) crash about `term` not being in the environment ```f* open FStar.Tactics type s (x:int) =...
I cloned the FStar repo and built F* from source on my Mac x86. I'm trying to build `examples/hello` using the instructions from [Executing F* code](https://github.com/FStarLang/FStar/wiki/Executing-F*-code), but this fails: ```...
```fstar module ProdAssoc let t1 = int * int * int let t2 = int * int & int let t3 = int & int * int let t4 =...
I have been trying to install HEAD (or other more recent releases not yet available on opam) in an opam switch. Due to way the build and installation is currently...
