Timeline for Strong induction on ℕ with function α → ℕ
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 17, 2022 at 12:39 | comment | added | Andrej Bauer | Thanks for the tip! | |
| Mar 17, 2022 at 12:02 | comment | added | Eric♦ |
You don't need the @ on that last line, exact nat.lt_wf.fix Qstep (f a) a rfl works too.
|
|
| Mar 15, 2022 at 10:35 | comment | added | burek | Excellent, exactly what I needed, thank you. | |
| Mar 15, 2022 at 10:34 | vote | accept | burek | ||
| Mar 14, 2022 at 23:03 | history | answered | Andrej Bauer | CC BY-SA 4.0 |