coq - 避免在 Coq 中使用 Proof General 打印符号
问题描述
在 DeepSpec 2018 的第 6 讲中,讲师检查了
string_dec
获得:
string_dec
: forall s1 s2 : string, {s1 = s2} + {s1 <> s2}
然后他继续查看 + 的定义,但在此之前,他在 CoqIde 中禁用了符号的打印。这样 sumbool 就被打印出来了。可以检查最后一个符号。
我怎样才能用 Proof General 做同样的事情?
解决方案
您可以使用菜单,Coq > OPTIONS > Set Printing All
。
您也可以直接发出命令,Set Printing All.
在运行 Check 命令之前在缓冲区中键入和评估它。这也使您可以访问Unset Printing Notations
仅禁用打印符号(您可以使用 CoqIDE 中的菜单执行此操作)。完成后,您可以删除此命令,这将撤消其效果。
最后,你也可以直接使用Coq > OTHER QUERIES > Check (show all)
on string_dec
。
推荐阅读
- swift - 如何创建用户可以在其上添加精确点的 3d 地球?
- python - 在 netCDF4 Python 中使用 date2num 转换日期时间时出错
- json - System.Text.Json.JsonSerializer.Serialize 将返回字符串括在双引号中
- linq - 将 if 和 foreach 语句转换为 linq 中的 select 和 where
- r - r中一个变量的折线图,如何着色?
- angular - *ngif Angular 和 IONIC 5 的属性绑定错误
- pdf - PDF大小的详细信息?
- time - 如何在 Odata V2 中将 Edm.String 类型的属性转换为数字
- mysql - 如何进行 MySQL 查询以检查该列是否是另一个字符串的开头
- c# - 无法将散列密码字节数组转回字符串