Hi all,

I can get most information about an inductive predicate in HOL by using `Inductive.the_inductive`

— but that does not seem to contain the number of inductive parameters that was given in the definition (or any other information about them). Anyone know of a way to get that information?

mmh, isn't that information contained in the type?

You mean the type returned by `the_inductive`

? I don't think it is — it returns a value of type `info`

, which is defined as `{names: string list, coind: bool} * result`

, with `result`

being `{preds: term list, elims: thm list, raw_induct: thm, induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}`

. Of course the number of parameters is *indirectly* contained in e.g. the induction rule `induct`

, but reconstructing it from that seems very brittle (not to mention hacky), and I'm not sure how to do it reliably.

Last updated: Dec 07 2023 at 16:21 UTC