Timeline for Inductive vs. recursive definitions
Current License: CC BY-SA 4.0
2 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 30, 2023 at 10:56 | comment | added | Jason Rute |
This question asks about the intersection of the two cases where you are defining a function from an inductive type to a universe (usually Prop) that has both a natural Inductive type constructor definition and a natural Fixpoint definition. (If you replace Prop with Bool, then Fixpoint would be the way to go of course.)
|
|
| Apr 30, 2023 at 8:14 | history | answered | Julien Puydt | CC BY-SA 4.0 |