Adds the add_ginductive hook for producing nested/mutual inductive types, as well as regular inductive types with all the fancy features you normally get from the inductive command (by contrast to add_inductive which only gives you a really basic inductive with no lemmas that doesn't work with the equation compiler or induction tactic).
digama0
commented
5 years ago
Adds the
add_ginductivehook for producing nested/mutual inductive types, as well as regular inductive types with all the fancy features you normally get from theinductivecommand (by contrast toadd_inductivewhich only gives you a really basic inductive with no lemmas that doesn't work with the equation compiler orinductiontactic).