Stream: MetaCoq

Topic: Necessary fields for tmMkInductive'


view this post on Zulip Basile Gros (Jan 25 2024 at 09:44):

Hello,
I was working with tmMkInductive' to create an inductive in the global context from a mutual_inductive_body, and I notices that the field for the number of parameters of the inductive, ind_npars, was deduced correctly by the call.
Is there a place to learn what fields are necessary for the tmMkInductive' call, and which are deduced from the structure given in argument ?

view this post on Zulip Yannick Forster (Jan 25 2024 at 09:46):

I'm afraid the only idea I have is to look at the OCaml code. It might be quite readable, but also potentially it might not make explicit what is inferred

view this post on Zulip Basile Gros (Jan 25 2024 at 09:46):

I see, thank you.


Last updated: Jul 23 2024 at 21:01 UTC