Timeline for Strong induction on ℕ with function α → ℕ
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 27, 2022 at 22:49 | comment | added | Eric♦ |
I do wonder if induction h : _ should handle the subst and rfl automatically, but haven't thought about it very hard.
|
|
| Mar 27, 2022 at 22:48 | comment | added | Eric♦ | Indeed; though I was trying to be less cryptic than Andrej's answer, not more! | |
| Mar 27, 2022 at 22:19 | comment | added | Kyle Miller |
If terseness is wanted, everything after the induction line can be replaced by subst hn, exact ind _ (λ b fb_lt_fa, ih _ fb_lt_fa _ rfl)
|
|
| Mar 17, 2022 at 13:16 | history | edited | Eric♦ | CC BY-SA 4.0 |
added 56 characters in body
|
| Mar 17, 2022 at 12:40 | history | answered | Eric♦ | CC BY-SA 4.0 |