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?

Those functions have bodies, and those give them computation rules.

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).

You can also use `Print T_rect.`

to see the definition of it.

Ah, that helps a lot. Thank you both!

Raymond Baker has marked this topic as resolved.

Last updated: Oct 01 2023 at 19:01 UTC