基本上，Lean 中只有两个命题：True 和 False。
命题外延性公理 (propext) 允许命题在逻辑上等价时被视为相等，并且每个真命题在逻辑上等价于 True。
类似地，每个假命题在逻辑上都等价于False。
True 是一个归纳定义的命题，具有不带参数的单个构造函数。
总是可以证明 True。
另一方面，False 是一个没有构造函数的归纳定义命题。
证明它需要找到当前上下文中的不一致之处。
True 和 False 都是 子单例；这意味着它们可以用来计算非命题类型的居民。
对于 True，这相当于忽略证明，该证明没有提供任何信息。
对于 False，这相当于证明当前代码无法访问并且不需要完成。
True is a proposition and has only an introduction rule, True.intro : True.
In other words, True is simply true, and has a canonical proof, True.intro
For more information: Propositional Logic
True.intro : True
True is true, and True.intro (or more commonly, trivial)
is the proof.
False is the empty proposition. Thus, it has no introduction rules.
It represents a contradiction. False elimination rule, False.rec,
expresses the fact that anything follows from a contradiction.
This rule is sometimes called ex falso (short for ex falso sequitur quodlibet),
or the principle of explosion.
For more information: Propositional Logic
False.elim : False → C says that from False, any desired proposition
C holds. Also known as ex falso quodlibet (EFQ) or the principle of explosion.
The target type is actually C : Sort u which means it works for both
propositions and types. When executed, this acts like an "unreachable"
instruction: it is undefined behavior to run, but it will probably print
"unreachable code". (You would need to construct a proof of false to run it
anyway, which you can only do using sorry or unsound axioms.)
f 定义中的第四个分支无法访问，因此不需要提供具体的 String 值：
def f (n : Nat) : String :=
if h1 : n < 11 then
"Small"
else if h2 : n > 13 then
"Large"
else if h3 : n % 2 = 1 then
"Odd"
else if h4 : n ≠ 12 then
False.elim (n:Nath1:¬n < 11h2:¬n > 13h3:¬n % 2 = 1h4:n ≠ 12⊢ False All goals completed! 🐙)
else "Twelve"
在此示例中，False.elim 向 Lean 指示当前本地上下文在逻辑上不一致：证明 False 足以放弃该分支。
类似地，g 的定义似乎有可能是非终止的。
但是，递归调用发生在程序中无法到达的路径上。
用于生成终止证明的证明自动化可以检测到局部假设是否不一致。
def g (n : Nat) : String :=
if n < 11 then
"Small"
else if n > 13 then
"Large"
else if n % 2 = 1 then
"Odd"
else if n ≠ 12 then
g (n + 1)
else "Twelve"
termination_by n