如何解决打印 ssrnat 的“.+1”定义
在 Ilya Sergey 的 Programs and Proofs 中,引入了 ssrnat
的命令 .+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
之类的东西。
如果您想了解更多相关信息,我鼓励您查看文档。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。