Raymond Baker (Feb 20 2022 at 07:41): Raymond Baker (Feb 20 2022 at 07:41):When defining an inductive type T in Coq, Coq automatically generates functions T_rect and T_ind. Are there computation rules for these functions, or how exactly are these functions defined?
In something like the HoTT book, when the induction and recursion principles for and inductive type are given, they are also given with computation rules, i.e., how the induction principle acts on a constructor of the type. What is the analogue of this in Coq?
Paolo Giarrusso (Feb 20 2022 at 08:15):Those functions have bodies, and those give them computation rules.
Paolo Giarrusso (Feb 20 2022 at 08:20):In Coq, the core primitives are pattern matching and hstructural recursion, and induction principles are defined on top. That is more or less equivalent (modulo a few complications of interest to experts).
Théo Winterhalter (Feb 20 2022 at 08:39):You can also use Print T_rect. to see the definition of it.
Raymond Baker (Feb 20 2022 at 09:07):Ah, that helps a lot. Thank you both!
Notification Bot (Feb 20 2022 at 09:07):Raymond Baker has marked this topic as resolved.
Last updated: Oct 01 2023 at 19:01 UTC