Why not to consistently adopt the convention used for projections also for constructors?
I wonder whether we could not put more basic small-size data in the inductive argument of Ind and 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_nparams with mind_nparamdecls (by analogy with mind_nrealargs and 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, ...
beware with cluttering these datatypes with caches though, since it's likely to end up in the vo file
while constructor type substitution should probably be cached (I see it pop from time to time in the profiler) I'm quite dubious about anything else you mention
It is probably not critical if small data (integers and strings) are duplicated in the vo files, knowing that arguments to
Construct are anyway shared, so it would be one copy per file.
As for having more precomputed data in the
mutual_inductive_body it would be only in the file defining the corresponding inductive types. I would be surprised that it leads to overheads, on the contrary. (It is quite a burden to always have to do low-level context carvings that are basically standard.)
Last updated: Oct 16 2021 at 09:07 UTC