Coq定理中的“参数”和“索引”有什么区别吗？

Question

我非常熟悉在声明归纳类型时区分参数和索引的处理。我不确定的是，在声明定理时，将内容放在冒号之前和之后是否有任何区别。具体

Lemma par (n : nat) : n < 1 -> n = 0.

Lemma ind : forall (n : nat), n < 1 -> n = 0.

我发现的一个区别是，在证明

par

时，冒号右侧的所有内容最初都在上下文中，而在

ind

中我必须

intro

它。您还知道这两者之间还有其他区别吗？你能举个例子说明它比一堆

intro

/

revert

更重要吗？

我担心的一个问题是，自动化可能会更喜欢其中一种，例如

autorewrite

或

auto

，尽管我找不到会产生影响的示例。

Answer 1

请参阅文档：

形式

Definition ident binders : type := term

相当于

Definition ident : forall binders, type := fun binders => term

。