Timeline for Is the validity of induction in Coq axiomatic?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 10 at 18:37 | vote | accept | alphie k | ||
| Jun 9 at 21:44 | history | became hot network question | |||
| Jun 9 at 17:53 | answer | added | Andrej Bauer | timeline score: 2 | |
| Jun 9 at 14:44 | answer | added | L. Garde | timeline score: 2 | |
| Jun 9 at 14:24 | comment | added | Trebor♦ |
If you want to see what axioms a proof uses, try Print Assumptions.
|
|
| Jun 9 at 10:49 | comment | added | JoJoModding |
Print nat_ind shows you the definition. The principle is derived using guarded recursion.
|
|
| S Jun 9 at 10:20 | review | First questions | |||
| Jun 9 at 18:08 | |||||
| S Jun 9 at 10:20 | history | asked | alphie k | CC BY-SA 4.0 |