变量的值是它类型的证明

林一二2024年06月20日 01:48

Lean 中的定理类似变量,它的类型就是传统的书上写的定理式子(但在Lean里,定理是它的名字,具体的公式什么的只是类型(也称为事实))。

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

theorem easy : 2 + 2 = 4 :=
  rfl

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

Code
Lean 中的定理类似变量,它的类型就是传统的书上写的定理式子(但在Lean里,定理是它的名字,具体的公式什么的只是类型(也称为事实))。

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

```lean
theorem easy : 2 + 2 = 4 :=
  rfl
```

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