fstar - 如何显示 fstar 表达式的值和/或类型?
问题描述
我正在使用 emacs fstar 模式浏览 fstar 教程。有没有办法评估表达式或其类型?
我正在寻找的是相当于精益的#check 或#eval。
解决方案
在 fstar-mode.el,F* 的 emacs 模式,你可以做
- Cc Cs Ce:计算表达式
- Cc Cs Cd:显示标识符的类型和文档
运行 fstar-mode.el 时,可以从 emacs 菜单栏中的 F* 菜单中找到这些和其他实用程序
推荐阅读
- python-3.x - 通过 jenkins 触发的 python3 脚本,该脚本利用 gitpython git.Repo 未显示所有分支
- javascript - AOS(滚动动画)元素在静态站点上不可见
- elasticsearch - 将 Kibana 连接到 Keycloak 时出现许可错误
- tkinter - AttributeError: '_tkinter.tkapp' 对象没有属性 'root'
- javascript - 未获取数据(React-redux)
- matlab - 如何将 MatLab 代码中的数据修改为 csv 文件
- python - 如何在 pandas DataFrame 中找到第二个最小值的索引?
- javascript - 如何使用单行从字符串中提取特定子字符串
- sql - 如何在 Postgresql 中创建条件插入函数?
- laravel - 在 Laravel 的不同列中按日期排序