reflexive inductive types

[nomeata]

While extending the section on structural recursion I was about to make a reference to reflective inductive types.

Adam Chilapa defines them in http://adam.chlipala.net/cpdt/html/InductiveTypes.html as:

A kind of inductive type called a reflexive type includes at least one constructor that takes as an argument a function returning the same type we are defining.

Not a pressing request, but at some point this ought to be discussed in the section on inductive types, and then probably also get a mention and example in the section on structural recursion.