Seeing these comments let me remark that the problem that I have with inductive definitions is that one could have the expectation that the foundations of mathe

Seeing these comments let me remark that the problem that I have with inductive definitions is that one could have the expectation that the foundations of mathematics would be a rather small and simple set of rules from which the rest can be derived. When one introduces inductive definitions as is done in coq this principle is out of the window. The branches of an inductive must satisfy a 'positivity condition' that is quite complicated. Then there is the thing that one can also do mutually recursive inductive definions. Then there are more rules for what kind of match statements are allowed. And let us not even get started on CoInductive definitions. IIRC Freek Wiedijk described the foundations as they are in coq as 'beyond baroque' and that is quite to the point.