Lasse Blaauwbroek (Feb 11 2021 at 02:42): 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...
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?
Gaëtan Gilbert (Feb 11 2021 at 10:36):something like that
Gaëtan Gilbert (Feb 11 2021 at 10:37):also you can repeat parameter names and named_context doesn't work with that
Lasse Blaauwbroek (Feb 11 2021 at 13:46):Ah yes, that makes sense, thanks
Last updated: Oct 13 2024 at 01:02 UTC