Stream: Coq devs & plugin devs

Topic: Inductive relative context


view this post on Zulip Lasse Blaauwbroek (Feb 11 2021 at 02:42):

I'm looking at the OCaml definition of inductive types here: https://github.com/coq/coq/blob/9178058af93e317a1d4ef1972fb426cbdefbac3f/kernel/declarations.ml#L229 Can anybody tell me why mind_params_ctxt is a Constr.rel_context and not a Constr.named_context? I have been unable to produce any inductive type that contains an anonymous variable (an error is generated when you do). I can use an anonymous variable when declaring a param like `(_:A), but then Coq just generates the name H for me...

view this post on Zulip Lasse Blaauwbroek (Feb 11 2021 at 03:09):

Ah, I now think I see the reason: Fields like mind_arity_ctxt also include the parameters, and since they are encoded as de Bruijn indices there it is more convenient to encode them as de Bruijn indices in mind_params_ctxt as well. Is that correct?

view this post on Zulip Gaëtan Gilbert (Feb 11 2021 at 10:36):

something like that

view this post on Zulip Gaëtan Gilbert (Feb 11 2021 at 10:37):

also you can repeat parameter names and named_context doesn't work with that

view this post on Zulip Lasse Blaauwbroek (Feb 11 2021 at 13:46):

Ah yes, that makes sense, thanks


Last updated: Mar 28 2024 at 12:01 UTC