helm/ocaml/cic_proof_checking/doc/inductive.txt

   1 Table of allowed eliminations:
   2
   3             +--------------------+----------------------------------+
   4             |   Inductive Type   |    Elimination to                |
   5             +--------------------+----------------------------------+
   6             | Sort | "Smallness" | Prop | SetI | SetP | CProp| Type |
   7             +--------------------+----------------------------------+
   8             | Prop     empty     | yes    yes    yes    yes    yes  |
   9             | Prop     unit      | yes    yes    yes    yes    yes  |
  10             | Prop     small     | yes    no2    no2    no2    no12 |
  11             | Prop               | yes    no2    no2    no2    no12 |
  12             | SetI     empty     | yes    yes    --     yes    yes  |
  13             | SetI     small     | yes    yes    --     yes    yes  |
  14             | SetI               | yes    yes    --     no1    no1  |
  15             | SetP     empty     | yes    --     yes    yes    yes  |
  16             | SetP     small     | yes    --     yes    yes    yes  |
  17             | SetP               | na3    na3    na3    na3    na3  |
  18             | CProp    empty     | yes    yes    yes    yes    yes  |
  19             | CProp    small     | yes    yes    yes    yes    yes  |
  20             | CProp              | yes    yes    yes    yes    yes  |
  21             | Type               | yes    yes    yes    yes    yes  |
  22             +--------------------+----------------------------------+
  23
  24 Legenda:
  25   no: elimination not allowed
  26   na: not allowed, the inductive definition is rejected
  27
  28   1 : due to paradoxes a la Hurkens
  29   2 : due to code extraction + proof irreleveance incompatibility
  30       (if you define Bool in Prop, you will be able to prove true<>false)
  31   3 : inductive type is rejected due to universe inconsistency
  32
  33   SetP : Predicative Set
  34   SetI : Impredicative Set
  35
  36   non-informative : Constructor arguments are in Prop only
  37   small : Constructor arguments are not in Type and SetP and CProp
  38   unit : Non (mutually) recursive /\ only one constructor /\ non-informative
  39   empty : in Coq:    no constructors and non mutually recursive
  40           in Matita: no constructors (but eventually mutually recursive
  41                      with non-empty types)