From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 3 Nov 2005 14:21:27 +0000 (+0000)
Subject: added documentation on allowed eliminations
X-Git-Tag: V_0_7_2_3~148
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aaf75c2cff13515b049a15cc8a96734e8967ae9b;p=helm.git

added documentation on allowed eliminations
---

diff --git a/helm/ocaml/cic_proof_checking/doc/inductive.txt b/helm/ocaml/cic_proof_checking/doc/inductive.txt
new file mode 100644
index 000000000..4cc9cade6
--- /dev/null
+++ b/helm/ocaml/cic_proof_checking/doc/inductive.txt
@@ -0,0 +1,40 @@
+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 : no contructors and (in Coq) non mutually recursive
+