什么是Coq中“定义”和“Let”的区别?为什么有些定义需要证明呢?
例如,这是群论中g1.v文件中的一段代码。
这个证明的目的是什么?
Definition exp : Z -> U -> U.
Proof.
intros n a.
elim n; clear n.
exact e.
intro n.
elim n; clear n.
exact a.
intros n valrec.
exact (star a valrec).
intro n; elim n; clear n.
exact (inv a).
intros n valrec.
exact (star (inv a) valrec).
Defined.
这个证明的目的是什么?
Let
在Section
结束后不会保留,而Definition
会。因此,在其所属的部分之外,你不能通过名称引用Let
定义的内容。 - Arthur Azevedo De Amorim