Questions tagged [fstar-mode]

As we know, we have "auto" (proof search) in Agda (Ctrl+c Ctrl+a in Emacs) as well as Idris as well as Coq, but when I was digging into F*'s Emacs mode, I failed to find a similar functionality. Does F* have this feature? If so, how can I use it?

I would like to debug simple F* program using Emacs fstar-mode and gdb. At the very end of the wiki of fstar-mode https://github.com/FStarLang/fstar-mode.el is information: The fstar-gdb command (M-x) attaches GDB to the current F* process and…

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.