FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
- Arity mismatch on let rec annotation - (explain) Should do with an error message number and in my case I got it by modifying a let rec with two...
// A tiny lexical bug in an error report, - not followed. module LexicalPopBug #push-options "--split_queries always" let oneisone (): Lemma (ensures 1 = 1) = () #pop-option /// *...
FST and ML for unix. Added a FDString for string files (useful in test). Added a printable class for unix. Made printable float and double print as #float and #double...
The docs suggest that this should work. I can't see where page search is configured. But it should find all pages that have any keyword by default please.
It would be good, but by no means of priority, to test catching and printing of these two basic errors from OCaml. We can catch them but not print them...
Setup: A.fst: ```fstar module A let a = "A.a" let b = "A.b" ``` B.fst: ```fstar module B let a = "B.a" let b = "B.b" include A {a} ```...
Consider the following minimal code snippet (done with @W95Psp and @TWal) ```fstar assume val p: int -> int -> prop assume val test: x:int -> y:int -> Lemma (p x...
