Timeline for Coq: defining more than two mutually recursive functions on inductive type
Current License: CC BY-SA 3.0
2 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 7, 2016 at 8:48 | comment | added | Khan | There is one method as shared in the link in post, however, it is for two mutually recursive functions. The problem is, to generalize it to more than two functions. Your suggested method will make the proofs difficult, as we won't be able to use list related lemmas from the library. | |
| Sep 7, 2016 at 7:05 | history | answered | Vinz | CC BY-SA 3.0 |