my blog https://overreacted.io
oopsie
+1
-1
+1
-1
public/beyond-booleans/index.md
+1
-1
public/beyond-booleans/index.md
···
396
396
397
397
```lean
398
398
def claim1 : Prop := 2 = 2 /- or := Eq 2 2 -/
399
-
def proof1 : claim1 := by rfl /- or := Eq.rfl 2 -/
399
+
def proof1 : claim1 := by rfl /- or := Eq.refl 2 -/
400
400
```
401
401
402
402
The `by rfl` tactic produces a proof `Eq.refl 2`, which is of type `Eq 2 2` (or the nicer `2 = 2`), which itself is a value of type `Prop`. Types pass, so it's proven: