相当于 Coq 的 Agda 的 `Eval`
相关标签：
Coq 有一个Eval命令，您可以使用该命令让类型检查器评估表达式并将其打印到控制台。在 Agda 中是否有与此等价的功能？特别是，我想避免实际编译和执行程序。在我开始编写证明之前，我只想自省一个值以确保我的代码正常工作（并帮助我更好地理解它）。
如果解决方案涉及 agda-mode（与 Coq 相比，它是语言的一部分），那很好。
特别声明：以上内容（图片及文字）均为互联网收集或者用户上传发布，本站仅提供信息存储服务！如有侵权或有涉及法律问题请联系我们。
举报
