FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
When you access the tutorial found at [https://www.fstar-lang.org/tutorial/](https://www.fstar-lang.org/tutorial/), the first module you see in the right pane is `module Welcome`. However, the text: ``` module Welcome (* This interface allows...
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)...
The `lookup` request is the only one which does not return any response if the request failed. This makes it hard to support it in a generic API for IDE...
Consider the following four files: ```fstar // A.fsti module A val t: Type0 val s0: Type0 // We wrap the type in a match to trigger automatic coercion. inline_for_extraction let...
```fst type vec (a: Type) : n: nat -> Type = | Nil : vec a 0 | Cons : #n: nat -> hd: a -> tl: vec a n...
When trying to bootstrap F* using Nix, `.#fstar-ocaml-snapshot` fails to build, throwing the following error: ``` * Error 54 at /nix/store/4skgqa9fayjbaw5fklzp2prj5q27nag6-fstar-0806a005a879f256ff5af6736fbea4d45ea6f6ca/lib/fstar/prims.fst(477,30-477,31): - a is not equal to the expected type...
Amos Robinson wants to put in a let that won't unfold but did not know how to build. Liking a clean build, I tried it for the first time on...
This PR improves the Nix code in various ways. List of changes: - centralize the Nix expressions in `.nix/` - use z3 4.8.5 as defined in nixpkgs - propagate the...