0

在 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打印定义？

注意：如果不可能，解释为什么也可以作为答案（以及命令的代码/工作的资源）。

4

1 回答 1

3

要打印符号，例如.+1您必须使用引号。

Print ".+1".

如果这样做，您最终将得到与Print nat.打印归纳类型的构造函数时相同的结果。事实上，你得到的结果是Print S.因为.+1是它的一个符号。

对于符号，通常你想使用Locate：

Locate ".+1'.

这一次的输出信息量更大：

Notation
"n .+1" := S n : nat_scope (default interpretation)

符号与定义不同。这只是一种编写和打印表达式的方式，但在它下面是相同的。

澄清一下，.+1是一个符号，而不是一个命令。命令是诸如等之类的东西。如果您想了解更多信息，我鼓励您查看文档Definition。Print

于 2021-01-28T07:41:35.337 回答