Timeline for How to write a proof of n + 0 = n in Lean 4 using the built in definition of addition for Nats and not the theorem for Nat.add_zero?
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 28 at 4:20 | comment | added | Chris Bailey |
Maintaining a 1:1 mapping where (a : Nat) + 0 = 0 is canonically (and potentially only) associated with the equational lemma for Nat.add, (a : Nat) * 1 = a with the equational lemma for Nat.mul, etc.
|
|
| May 28 at 3:08 | comment | added | Charlie Parker | what do you mean by the direct approach? | |
| May 28 at 1:30 | history | edited | Chris Bailey | CC BY-SA 4.0 |
added 366 characters in body
|
| May 28 at 1:23 | history | answered | Chris Bailey | CC BY-SA 4.0 |