Lean4 中的未知标识符“开始”

Question

我在 VSCode 中的 Lean4 中输入了以下内容：

example (p q r : Prop) : ((p ∨ q) → r) ↔ ((p → r) ∧ (q → r)) :=
begin

它告诉我“未知标识符‘开始’”。当我向下输入

end

两行时，它告诉我“无效的‘结束’，范围不足”。我究竟做错了什么？是不是我没有正确设置Lean？

Answer 1

开始/结束块是精益 3 语法。 Lean 4 中进入战术模式的关键词是

by

，如下：

example (p q r : Prop) : ((p ∨ q) → r) ↔ ((p → r) ∧ (q → r)) := by sorry

不再有与

end

类似的东西，因为它现在依赖于空白，但有一个可选的

done

终结器，如果目标实际上并未关闭，它将成为错误。

即使您经常使用精益 3，我也建议您略读手册和/或精益/精益函数式编程中的定理证明（请参阅手册中的第 4 章和第 5 章），因为已经有了重大的更改和改进。