FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
Hi, This PR adds a rule to the parser and adds a node `PatVQuote` to the surface AST so that ```%foo`` is now a legal pattern. `PatVQuote` nodes are desugared...
This PR exposes the `unascribe` normalisation step. It can be useful to get more readable terms and it also seems to speed up some normalisations. I have just exposed the...
F* (https://github.com/FStarLang/FStar/commit/5bcd16865e5161ccbc7b2b9ead96ba099618adf8) does not seem to retypecheck the parameters of the effect combinators when they are used. This is probably intentional since it notably avoids rechecking the monotonicity of `pure_wp`...
That allow have gradually increase version until we have stable infra.
Let's say you want write lens in F* and export that as library to F#. Currently exportation process encode operators as functions which make code looks unnecessary ugly. Original code...
Hi, I was using the reflection API in a total context and found some `inspect_*` primitive were lacking refinements, forcing me to add `admit`s about termination of some of my...
Companion PR in https://github.com/FStarLang/karamel/pull/273 You can override the definition of `KRML_HOST_IGNORE` with something more suitable if need be by invoking `krml` with `-add-early-include '"mydefs.h"'`, then defining `KRML_HOST_IGNORE` in `mydefs.h` before...
`M4` is a layered effect and I try to write something like: `reify (M4?.reflect x) == x`. I am not sure if this is the correct way to do it,...
Recently I managed to prove `False` by accident while using `reify` for an indexed effect. I tried to minimize it in a PoC (with some help from @TheoWinterhalter), but it...
This PR implements a suggestion by @R1kM : provide a SteelGhost function, `sldump`, to print the current vprop at type-checking time. For instance, the code below (available in this PR...
