fstarfstar-mode

How can I display the value and/or type of an fstar expression?


I'm going through the fstar tutorial using the emacs fstar-mode. Is there a way to evaluate an expression or its type?

What I'm looking for is an equivalent to Lean's #check or #eval.


Solution

  • In fstar-mode.el, the emacs mode for F*, you can do

    These and other utilities can be found from the F* menu in the menu bar of emacs when running fstar-mode.el