FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
Without that I'm getting a new error: ``` $ make -C examples make: Entering directory '/home/hritcu/Projects/fstar/pub/examples' Makefile.include:11: /home/hritcu/Projects/fstar/pub/bin//../lib/fstar/gmake/fstar.mk: No such file or directory make: *** No rule to make target...
To reproduce, either check out my [entire CuteCAS repository](https://github.com/hacklex/CuteCAS), or just get the following files from it: - AlgebraTypes.fst - Fractions.Definition.fst - Fractions.Equivalence.fst - Fractions.Addition.fst - Fractions.Multiplication.fst - Fractions.fst Then...
During attempt to troubleshoot #2539 ``` ~/FStar$ date ; bin/fstar.exe ../CuteCAS/Fractions.fst --include ../CuteCAS --cache_dir cas_current --lax ; date Mon Apr 18 21:29:46 +06 2022 /home/kant/FStar/ulib/FStar.Classical.fsti(0,0-0,0): (Warning 241) Unable to load...
Windows. Install FStar.exe from https://github.com/FStarLang/FStar/releases/tag/v2022.03.24 and from https://github.com/FStarLang/FStar/releases/tag/v2022.01.15 When using https://marketplace.visualstudio.com/items?itemName=artagnon.vsfstar which simply run `fstar.exe --lsp` I see following error in the Output of VS Code. ``` [E] Failed to...
On a steel example similar to the one given for [PR#2534](https://github.com/FStarLang/FStar/pull/2534), fstar still fails to rewrite a vprop with an `smt_fallback` and raises a typing error: ```fstar module Mem =...
This function was failing in my environment and it seems to fix it. This is checking just the prefix of the output rather than the whole of it. Context: I...
Based on my tests and conversation from https://github.com/FStarLang/FStar/issues/2344 F* does not yet support Z3 4.8.11. Are there any plans as of now to port to newer versions?
When run this code in sandbox ``` module Welcome // open FStar.Mul let sqr_is_nat (x:int) : unit = assert (x * x >= 0) ``` I receive this error ```...
Consider this module ``` module FStar.Preorder type relation (a : Type) = a -> a -> Type0 let reflexive (#a:Type) (rel:relation a) = forall (x:a). rel x x ``` Hover...
This PR adds: - Steel.C.Connection: PCM morphisms and PCM connections, which are a generic way of relating a PCM for a part of a structure to a PCM for the...
