如何在FStar中查看表达式的值与类型，等效Lean的#check/#eval

在Emacs的fstar-mode中，对应Lean的#check、#eval功能的操作方式如下：

• 代码内查询：在编辑区对应位置写入 #check <目标表达式>，将光标移动到该行，按下fstar-mode默认快捷键 C-c C-n，minibuffer区域会直接输出该表达式的推导类型。
• 交互式查询：按下快捷键 C-c C-s 启动FStar交互式shell，直接在shell输入框中输入 #check <目标表达式> 后回车，即可得到类型结果，不需要修改代码文件内容。

• 代码内求值：在编辑区对应位置写入 #eval <目标表达式>，光标移动到该行后按下 C-c C-n，minibuffer会返回表达式的求值结果。
• 交互式求值：在FStar交互式shell中直接输入 #eval <目标表达式> 回车，就能得到运行结果。

注意：查询或求值的表达式需要依赖当前文件的上下文时，要先确保表达式之前的代码已经通过FStar的检查，避免出现上下文未定义的报错。

内容的提问来源于stack exchange，提问作者azani