X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fcic_proof_checking%2Fdoc%2Finductive.txt;fp=components%2Fcic_proof_checking%2Fdoc%2Finductive.txt;h=f2e49d3987fb770d9d3e940dd4094583f41f9aca;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/components/cic_proof_checking/doc/inductive.txt b/components/cic_proof_checking/doc/inductive.txt
new file mode 100644
index 000000000..f2e49d398
--- /dev/null
+++ b/components/cic_proof_checking/doc/inductive.txt
@@ -0,0 +1,41 @@
+Table of allowed eliminations:
+
+            +--------------------+----------------------------------+  
+            |   Inductive Type   |    Elimination to                |
+            +--------------------+----------------------------------+
+            | Sort | "Smallness" | Prop | SetI | SetP | CProp| Type |
+            +--------------------+----------------------------------+
+            | Prop     empty     | yes    yes    yes    yes    yes  |
+            | Prop     unit      | yes    yes    yes    yes    yes  |
+            | Prop     small     | yes    no2    no2    no2    no12 |
+            | Prop               | yes    no2    no2    no2    no12 |
+            | SetI     empty     | yes    yes    --     yes    yes  |
+            | SetI     small     | yes    yes    --     yes    yes  |
+            | SetI               | yes    yes    --     no1    no1  |
+            | SetP     empty     | yes    --     yes    yes    yes  |
+            | SetP     small     | yes    --     yes    yes    yes  |
+            | SetP               | na3    na3    na3    na3    na3  |
+            | CProp    empty     | yes    yes    yes    yes    yes  |
+            | CProp    small     | yes    yes    yes    yes    yes  |
+            | CProp              | yes    yes    yes    yes    yes  |       
+            | Type               | yes    yes    yes    yes    yes  |
+            +--------------------+----------------------------------+
+
+Legenda:
+  no: elimination not allowed
+  na: not allowed, the inductive definition is rejected
+ 
+  1 : due to paradoxes a la Hurkens 
+  2 : due to code extraction + proof irreleveance incompatibility
+      (if you define Bool in Prop, you will be able to prove true<>false)
+  3 : inductive type is rejected due to universe inconsistency 
+  
+  SetP : Predicative Set
+  SetI : Impredicative Set
+
+  non-informative : Constructor arguments are in Prop only
+  small : Constructor arguments are not in Type and SetP and CProp
+  unit : Non (mutually) recursive /\ only one constructor /\ non-informative
+  empty : in Coq:    no constructors and non mutually recursive
+          in Matita: no constructors (but eventually mutually recursive
+                     with non-empty types)