coq - 定理蕴涵的coq语法

Question

我遵循本教程：https
://softwarefoundations.cis.upenn.edu/lf-current/Basics.html“重写证明”部分：
代码

Theorem plus_id_example : forall n m : nat,
  n = m =>
  n + n = m + m.

产生错误：
语法错误：'。' 预计在 [vernac:gallina] 之后（在 [vernac_aux] 中）。
我不明白我在做什么错？
另外，获取文档的最佳位置是什么？我的意思是，初学者友好的文档。

标签： coq

Answer 1