FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
Hello. `fstar --codegen FSharp` generates a number of F# files from the standard library of F*. I want to include them in the project. Is there a way to understand...
The following Steel definition is accepted in normal and in lax mode but not when loaded as a dependency: ```fstar module A open Steel.Effect noeq type fsteel (pre : pre_t)...
Verification proceeds really slowly when the typeclass tree is step or two above trivial... See my [ringlike algebraic structures](https://github.com/hacklex/CuteCAS/blob/master/FStar.Algebra.Classes.Ringlikes.fst), dependencies are * FStar.Algebra.Classes.Equatable * FStar.Algebra.Classes.Grouplike from the same repository (no...
See these examples: ```fstar open FStar.All open FStar.Tactics let f (): ML bool = true let fstar_all_ml_name: name = explode_qn "FStar.All.ML" // Destructing a ML comp cause problems [@@expect_failure] let...
When using `resolve_implicits`, there seems to be no option to control the order in which the different implicits are instantiated. This is needed when interacting with libraries (such as Steel)...
Hi, This PR adds a reflection for ranges, with to the following definitions : - a type `rng_view` furnishes a view for ranges - `inspect_range: range -> rng_view`; - `range_of_term:...
The following example verify without any issue when checked in normal mode: ```fstar module Main open FStar.Tactics let dummy_lemma (x : int) goal (pf : goal) : goal = pf...
See the following example: ```fstar module Test open FStar.Tactics val make_extraction_fail: unit -> Tac nat let make_extraction_fail () = let rec f (n:nat): Tac nat = if n = 0...
See the following code: ```fstar module UnitExtraction let byte = n:nat{n < 256} let lbytes (n:nat) = l:list byte{List.Tot.length l == n} // In my real case, everything is well-encapsulated...
This PR adds support for Nix and the Hydra based CI we are setting up with @W95Psp at INRIA. The first commit adds : - `*.nix` files and notably the...
