I have questions about the
For projections, we don't care about having the
PrimRecord field to recursively refer to the kernel name of the inductive block. But for constructors, recursive calls are represented with
Rels and a substitution by the actual
Ind needs to be done everytime we need the type of a constructor. Why not to consistently adopt the convention used for projections also for constructors? The drawback is that the
mutual_inductive_body refers to the name to which it is bound in the kernel but the advantage is that we save the process of substitution. Any opinion?
I wonder whether we could not put more basic small-size data in the
inductive argument of
Construct rather than having to query the env for simple things like the number of parameters, the name of the types and constructors, etc. Any opinions?
In a similar vein, I wonder whether more data could be precomputed in the
mutual_inductive_body. I'm thinking e.g. to complementing
mind_nparamdecls (by analogy with
mind_nrealdecls), or to add a version of the arity context with params already chopped, or a version of constructor contexts with params already chopped, ...
Last updated: Oct 21 2021 at 20:02 UTC