问题标签 [fstar-mode]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
fstar - 是否有 F* 的证明搜索功能？
正如我们所知，我们在 Agda（ Emacs 中的Ctrl+ c Ctrl+ a）以及 Idris 和 Coq 中都有“自动”（证明搜索），但是当我深入研究 F* 的 Emacs 模式时，我没有找到类似的功能.
F*有这个功能吗？如果是这样，我该如何使用它？
emacs - 带有 emacs 和 F* 的 Gdb
我想使用 Emacs fstar-mode 和 gdb 调试简单的 F* 程序。在 fstar-mode https://github.com/FStarLang/fstar-mode.el的 wiki 的最后是信息：
没有进一步的解释。
在 Emacs 中（假设我正在编辑 Test.fst 文件）我调用fstar-gdb命令并继续到gdb控制台我正在尝试使用命令file Test和run. 他们工作正常，但是break 3（或任何其他行）说它main.c（显然）找不到第 3 行。
如何gdb与 F* 一起使用？
fstar - 如何显示 fstar 表达式的值和/或类型？
我正在使用 emacs fstar 模式浏览 fstar 教程。有没有办法评估表达式或其类型？
我正在寻找的是相当于精益的#check 或#eval。