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...
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?
something like that
also you can repeat parameter names and named_context doesn't work with that
Ah yes, that makes sense, thanks
Last updated: Feb 05 2023 at 20:03 UTC