fstar - 如何显示 fstar 表达式的值和/或类型？

Question

我正在使用 emacs fstar 模式浏览​​ fstar 教程。有没有办法评估表达式或其类型？

我正在寻找的是相当于精益的#check 或#eval。

Answer 1

在 fstar-mode.el，F* 的 emacs 模式，你可以做

• Cc Cs Ce：计算表达式
• Cc Cs Cd：显示标识符的类型和文档

运行 fstar-mode.el 时，可以从 emacs 菜单栏中的 F* 菜单中找到这些和其他实用程序