printing - 打印 ssrnat 的 ".+1" 定义
问题描述
在 Ilya Sergey 的Programs and Proofs中,引入了ssrnat
's 命令.+1
并用于定义自然数上的一些函数。虽然它的用法在那里得到了很好的解释,但我也对它是如何定义的,更重要的是它是如何工作的很感兴趣。在那一章的前面介绍了nat
类型,我们可以用 " " 来验证定义Print nat.
,它产生:
Inductive nat : Set := O : nat | S : nat -> nat
然而,.+1
命令“ Print .+1.
”或“ Print +1.
”产生:
Syntax error: 'Fields' or 'Rings' or 'Hint' 'View' expected after 'Print' (in [command]).
甚至试图通过在其前面添加一个自然数来规避这一点,例如在 " Definition one: nat := 1.
" 后跟 " Print one.+1.
" 产生:
Syntax error: '.' expected after [command] (in [vernac_aux]).
但是,我想这个命令是在库中定义的,而不是语言的原语,所以感觉应该能够像其他任何人一样检查它的定义。
如果是这种情况,为什么命令不起作用以及如何.+1
打印定义?
注意:如果不可能,解释为什么也可以作为答案(以及命令的代码/工作的资源)。
解决方案
要打印符号,例如.+1
您必须使用引号。
Print ".+1".
如果这样做,您最终将得到与Print nat.
打印归纳类型的构造函数时相同的结果。事实上,你得到的结果是Print S.
因为.+1
是它的一个符号。
对于符号,通常你想使用Locate
:
Locate ".+1'.
这一次的输出信息量更大:
Notation
"n .+1" := S n : nat_scope (default interpretation)
符号与定义不同。这只是一种编写和打印表达式的方式,但在它下面是相同的。
澄清一下,.+1
是一个符号,而不是一个命令。命令是诸如等之类的东西。如果您想了解更多信息,我鼓励您查看文档Definition
。Print
推荐阅读
- python - PySpark,计算两个日期之间的天数
- c# - 如何从表单中获取字符串列表并使用 AJAX 将一些选项结果返回到下拉列表?
- java - Docker 容器自动退出,退出代码为 139
- php - CakePHP 3 补丁实体创建新的关联实体
- java - 在模型中进行排序忽略字段
- python - 如何在 Django 中检查并传递我的表单中的用户实例?
- charts - 此图中使用哪个图表
- java - 使用环境变量spring boot在dynamo db中动态设置全局二级索引名称
- php - 如何使用 Laravel 创建多级动态菜单?
- arrays - Dart:如何将简单的地图转换为 dart/flutter 中的列表?