patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
twk
danabra.mov
+2
public/beyond-booleans/index.md
+2
public/beyond-booleans/index.md
···
83
83
def proof1 : claim1 := by rfl
84
84
```
85
85
86
+
*([Try it in the Lean REPL.](https://live.lean-lang.org/#codez=CYUwZgBAxgNghgSwLYEYIC4IAUBOB7ABwwF4IAmCUsgKFEgPzzDU1kVRIgCMBPCHMDGpA))*
87
+
86
88
For now, don't worry about what `by rfl` really means; we'll get to that a bit later. Think of it as a built-in Lean value that can prove any statement like `foo = foo`.
87
89
88
90
However, look at the types! Like in the earlier example, `2 = 2` is of type `Prop`. But here's something strange: `by rfl` itself is of type `claim1` (which is `2 = 2`).