patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
twk
danabra.mov
+1
-1
public/beyond-booleans/index.md
+1
-1
public/beyond-booleans/index.md
···
32
32
33
33
34
34
35
-
*(Try it in the [Lean REPL](https://live.lean-lang.org/#codez=CYUwZgBAjgriDOAXAlgewHYQFwF4ICYIBqAiPAFgCgg) or [VS Code](https://lean-lang.org/install/).)*
35
+
*(Try it in the [Lean REPL](https://live.lean-lang.org/#codez=CYUwZgBAjgriDOAXAlgewHYEYIC4C8EATBAYQFCiSwIobH5EQDUjBALBeNHEmugMy5SzVhACsQA) or [VS Code](https://lean-lang.org/install/).)*
36
36
37
37
Let's annotate them explicitly so we remember that `2 + 2 = 4` is of type `Prop`:
38
38