Agda中是否有等价于Coq `Eval`命令的功能

Agda 完全支持你需要的「不编译执行程序、仅通过类型检查器求值查看表达式结构」的能力，最常用的实现依托 agda-mode 交互功能，不需要额外写执行入口、不需要走完整编译流程，归约结果和编译运行结果完全一致。

核心交互命令：求值到范式（完全对等 Coq Eval） #

这是日常用得最多的方式，操作非常简单：

• 你可以在代码任意位置打一个?创建交互洞，把光标移到洞内，输入你想要探查的表达式；也可以直接用鼠标/光标选中代码里已经写好的目标表达式
• 调用求值到正规式的命令：Emacs 版 agda-mode 默认快捷键是 C-c C-n（先按Ctrl+C，再按Ctrl+N），VS Code 版可以直接在命令面板搜索「Agda: Evaluate term to normal form」触发
• 触发后Agda的类型检查器会直接在输出区/迷你缓冲区打印表达式完全求值后的最简结构，全程不会生成可执行文件，也不会执行编译后的二进制，所有计算都在类型检查阶段完成。

其他辅助探查命令 #

除了全量求值到最简形式，还有几个高频使用的命令帮你快速核对代码逻辑：

• 查看表达式类型：快捷键C-c C-d，输入目标表达式后会直接返回它的类型，帮你快速确认写出来的代码类型是否符合预期
• 弱头范式求值：快捷键C-c C-w，只会剥掉表达式最外层的构造子，不会对内层做全量归约，适合探查结构特别复杂的大项，避免全量求值耗时太长
• 跳转查看定义：光标放在任意函数/构造子/数据类型名上，按M-.（Emacs）/ 编辑器右键跳转定义，可以直接对应到你写的原始定义代码

非交互场景的校验方法 #

如果你不想用交互模式，也可以直接在代码里写等式校验项：

-- 比如你要验证加法函数的逻辑是否正确
_ : 2 + 3 ≡ 5
_ = refl

Agda在检查refl的时候会自动对等号两边的表达式做归约，如果两边值不匹配，会直接在报错信息里打印两边归约后的实际结构，你可以直接从报错里看到你写的函数实际算出的结果是什么，以此核对逻辑。

小提示：上述所有归约都严格遵循Agda的类型论规则，和编译后运行的结果完全一致，你完全可以在正式写证明之前用这些方法快速试错，不用花很久写完证明才发现最开始的函数逻辑写错了。

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