FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
This avoids emitting no-op witness/recall calls in the generated code.
- [x] Move all modules to use the PCM-based memory model (Nik) - [x] Revise the formulation of frame preservation and remove the assume Steel.Effect.Atomic.witness_h_exists (Aseem) - [ ] Add...
Hello all, I like to convert all of my function declarations in the `val ...; let ... =` style, but doing so in a tutorial example (https://fstar-lang.org/tutorial/book/part1/part1_quicksort.html#generic-sorting) led to an...
Hello. Awesome work! I wanted to compile it to F#, but it'd need git submodules and not very nice. So I decided to make a nuget package, see [repo](https://github.com/WhiteBlackGoose/FStar.Lib.NET). It's...
We can currently define a `prop` type in various ways, for instance: ``` type prop = a:Type0{ forall (x:a). x === () } ``` or (maybe) better: ``` abstract let...
The following code works, I'm basically just giving another name to `Cons`: ``` val push : int -> list int -> Tot (s:(list int){Cons? s}) let push x xs =...
- [x] move the Low\* libraries under the LowStar prefix (instead of FStar) - [x] remove old libraries from ulib/ - [x] F\* doc (the tool) (#634) - [x] write,...
The following snippet doesn't work: ``` module JH type vec (a: Type): nat -> Type = | Nil: vec a 0 | Cons: hd:a -> n:nat -> tl:vec a n...
Hello, It appears that `unquote` fails when used in a proofstate with no goal. The following module definition shows the current behavior: `unquote`'s behavior depends on the current proofstate. ```fstar...
See the following minimal example ```fstar open FStar.Tactics assume val predicate: int -> Type0 // If we add the SMTPat, then `test` succeed assume val predicate_is_true_lemma: x:int -> Lemma (predicate...
