Stream: Coq users

Topic: ✔ Comuptation Rules for rect?


view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Feb 20 2022 at 08:15):

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

view this post on Zulip 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).

view this post on Zulip Théo Winterhalter (Feb 20 2022 at 08:39):

You can also use Print T_rect. to see the definition of it.

view this post on Zulip Raymond Baker (Feb 20 2022 at 09:07):

Ah, that helps a lot. Thank you both!

view this post on Zulip Notification Bot (Feb 20 2022 at 09:07):

Raymond Baker has marked this topic as resolved.


Last updated: Feb 04 2023 at 22:29 UTC