Timeline for When is the lean 4 "by" required?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 21 at 6:41 | history | edited | jthulhu | CC BY-SA 4.0 |
edited body
|
| Jun 20 at 23:44 | comment | added | Jason Rute |
@Penelope As this answer says calc is one of the few identifiers which works both as a tactic and as a term, so you can use it in either circumstance. Basically whenever you have := starting a proof then if you want to use tactics (which you probably want to do until you know more lean) use by.
|
|
| Jun 20 at 21:47 | comment | added | Penelope |
Can i use by at the end of the first line of a proof which essentially sets out the theorem to be proven (name, variable types, hypotheses, overall goal)? I've seen some proofs that have := by then calc on the next line, and some that don't := and have calc on the next line.
|
|
| Jun 12 at 20:25 | history | edited | jthulhu | CC BY-SA 4.0 |
added 1091 characters in body
|
| S Jun 12 at 16:47 | review | First answers | |||
| Jun 21 at 17:27 | |||||
| S Jun 12 at 16:47 | history | answered | jthulhu | CC BY-SA 4.0 |