]> matita.cs.unibo.it Git - helm.git/blob - components/cic_proof_checking/doc/inductive.txt
EXPERIMENTAL and _INCOMPLETE_ COMMIT:
[helm.git] / components / 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)