FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
I ran into an issue where normalization got stuck evaluating a mostly-concrete term. After talking on Slack, @nikswamy was surprised that normalization-by-evaluation stops under pattern matches. @mtzguido also suggested `zeta_full`...
The functional versions of x_intro/elim are used about twice as much as the introduce/eliminate sugar. And if you are generating propositions via functions, and the more serious projects do, you...
This adds some attributes and normalization tweaks to unfold more of the indirections introduced by typeclasses. The idea is to try to unfold methods when their dictionary is concrete, but...
From @TWal in https://github.com/FStarLang/FStar/pull/3094#issuecomment-1810450113 : > The bool and prop properties are causing a lot of redundancy in ulib, but is it needed? While I agree that we need to...
See the following example, discussed on Slack a week ago (putting it in an issue for posterity & tracking) ```fstar #set-options "--fuel 0 --ifuel 1" assume val ord: Type0 assume...
This fails, complaining that `f` has to be a function. ```fstar noeq type pack = { ff : Type u#a -> Type u#a; } let ty (a:Type) : Type =...
Probably not a big deal but: ```fstar // works let _ = let id : 'a -> 'a = fun x -> x in () // fails with: Identifier not...
In order to have better hygiene in my proofs, I tried to make a few of my functions opaque to SMT, in order to force F* to use their lemmas...
Example of after, in Pulse: previously this was all in a single line. If it fits in the line width, it will still be in a single line, but it...
