Meme of LinOnetwo

Lean 中的定理类似变量，它的类型就是传统的书上写的定理式子（但在Lean里，定理是它的名字，具体的公式什么的只是类型（也称为事实））。值就是证明过程，字符串变换、同义反复、套套逻辑。

变量的值就是其类型的证明，例如

theorem easy : 2 + 2 = 4 :=
  rfl

类型就是这个公式，值就是 rfl，证明了这个公式。