The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  This question is slightly vague:

  I want to understand:

  (*) what are the restrictions on inductive data types (it appears to be more subtle then "X can't appear in a negative position" i.e. "(X -> A) -> X" as a constructor)

  (*) how this relates to well-foundedness and termination

  What's a good resource to read up on for this?

  (Ideally, I'm looking for something short + rigorous).

Thanks!