FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
An example from @msprotz (use `--include karamel/krmllib`), not minimized yet ```fstar module J module B = LowStar.Buffer module U32 = FStar.UInt32 module S = FStar.Seq open FStar.HyperStack.ST let rec sum...
Originally ran into this trying to mix the Stack effect with a dependent record type; narrowed the reproduction case down to: ```fstar type pos = (len:nat & (n:nat { n...
This is not really observable (unless the printing raises an exception) but the typechecker will routinely render terms to put into error message guards, which is probably very wasteful. Giving...
The problem is described in the comments of the following code: ```fstar // Two monads, with returns and binds assume val m1: Type0 -> Type0 assume val m2: Type0 ->...
Similar to #3309, but using record disambiguation to bamboozle the type inference of F*: ```fstar // Two monads, with returns and binds assume val m1: Type0 -> Type0 assume val...
Test.fsti: ```fstar module Test ``` Test.fst: ```fstar module Test let x:int = 0 let y:int = Test.x ``` ``` $ fstar.exe Test.fst * Error 117: - You may have a...
Consider the following (minimized) F* code: ```fstar module State noeq type table_name (r: Type0) = { te: Type0; get: r -> Seq.seq te; } let return_table (#t: Type0) (tabs: t)...
@tahina-pro This is a PR to enable fstar to build on Windows/OCaml CI. It uses DkML, although I wrote it in a way that *should* be able to run with...
This allows F* to build with OCaml 5.2.0. Fixes #3048
This PR allows to tag certain type implicits with the `@@@unrefine` attribute, causing the unifier to attempt to peel away all refinements of the type before instantiating the uvar. With...