patricktree.me / overreacted
forked from danabra.mov/overreacted
my blog https://overreacted.io
fork atom

typo

danabra.mov b6b670fb dfd66dde

+1 -1
unified split
+1 -1
public/beyond-booleans/index.md
··· 180 180 181 181 *([Try it in the Lean REPL.](https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQOAmApgGZxhQQTECMcAXHAExwC8T9bWAnnFMeniKlylYswbMA1OzYAWDnG69+BEmQpVGAcnrtpzOQqVEAxsCKrhGsVp0S4+1nHl02MAO4QA+knz4vHt6EAI5exBAArlCCaiJUAMy6AHIQ8AAUUjJwAKwAlEY8puaEOEA))* 182 182 183 - In the above snippet, the values produced via `by decide`, `by rfl` and `two_add_two_eq_four` all values of the same `2 + 2 = 4` type: 183 + In the above snippet, the values produced via `by decide`, `by rfl` and `two_add_two_eq_four` are all values of the same `2 + 2 = 4` type: 184 184 185 185 ![Diagram: by decide, two_add_two_eq_four, and by rfl are all valid proofs of 2 + 2 = 4. Also, they are all equal.](./8.svg) 186 186