stuebinm (Aug 24 2022 at 10:49): stuebinm (Aug 24 2022 at 10:49):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?
Mathias Fleury (Aug 24 2022 at 14:29):mmh, isn't that information contained in the type?
stuebinm (Aug 24 2022 at 16:05):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: Apr 25 2024 at 16:19 UTC