patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
oops
danabra.mov
+1
-1
public/beyond-booleans/index.md
+1
-1
public/beyond-booleans/index.md
···
168
169
### Proof Irrelevance
170
171
-
It is worth noting that, just like a proposition may have *no* valid proofs, it may also have *many* proofs--in fact, as many as you like. For example, `2 + 2 = 4` can be proven `by rfl` but it can also be proven using an existing result from Mathlib (conveniently called `two_plus_to_eq_four`), or the more powerful `by decide`:
172
173
```lean
174
import Mathlib
···
168
169
### Proof Irrelevance
170
171
+
It is worth noting that, just like a proposition may have *no* valid proofs, it may also have *many* proofs--in fact, as many as you like. For example, `2 + 2 = 4` can be proven `by rfl` but it can also be proven using an existing result from Mathlib (conveniently called `two_add_two_eq_four`), or the more powerful `by decide`:
172
173
```lean
174
import Mathlib