Stream: Coq devs & plugin devs

Topic: `mutual_inductive_body` API

view this post on Zulip Hugo Herbelin (Aug 20 2021 at 16:02):

I have questions about the mutual_inductive_body API.

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 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, ...

Last updated: Oct 21 2021 at 20:02 UTC