Timeline for Is the validity of induction in Coq axiomatic?
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 13 at 11:02 | comment | added | Andrej Bauer | I believe the expression is "there's more than one way to skin a recursive cat". | |
| Jun 12 at 18:49 | comment | added | cody |
Originally, the correctness of the guard condition was made by showing that one can translate any fix defined function to one using the induction principles/recursion operators. So little bit of an ouroboros situation here.
|
|
| Jun 10 at 18:37 | vote | accept | alphie k | ||
| Jun 9 at 17:53 | history | answered | Andrej Bauer | CC BY-SA 4.0 |