Théophile Wallez
Théophile Wallez
Here is another minimized example that I stumbled upon, which uses a simple monad (state monad that doesn't fail) ```fstar #set-options "--fuel 0 --ifuel 0" assume val state: Type0 assume...
Interesting, thank you for the detailed answer! It definitely clashes with my internal model of F* hence I have a few follow-up questions. About ifuel and pairs: in my mind,...
Thank you for the detailed explanations! ifuel definitely didn't work as I expected. To test my new understanding, I tested the following example that works with an ifuel of 1...
I tested on my projects, I have a few queries on MLS* that started to split that were fixed by bumping rlimits. The fix works on my original problem, so...
There are also unnecessary parenthesis in expressions like `p /\ (let x = ... in ...)` and `p /\ (match x with ...)`, similar to the `forall` example!
I guess I am the Inria folk who like to treat warning as errors (sorry!), I can disable some more warnings if needed. I am doing this mainly because I...
No worries, didn't take that negatively!
This would also be very useful for projects that use DY* or Comparse! Everytime a directory is added to these projects, all projects that depend on them need their Makefile...
I didn't know `[@@coercion]`! What is it doing?
Ah excellent, thank you!