The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

The positivity criterion of the Calculus of Inductive Constructions is described in the Coq Reference Manual rather tersely:
  http://coq.inria.fr/distrib/current/refman/Reference-Manual006.html#sec199

(Other interesting and tricky things are described in this document, such as the sorting rules for pattern-matching results, including empty and singleton elimination).

On Mon, Oct 28, 2013 at 5:36 AM, t x <txrev319 AT gmail.com> wrote:

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!