...

[helm.git] / matita / matita / lib / extraction.ma

diff --git a/matita/matita/lib/extraction.ma b/matita/matita/lib/extraction.ma
index aa781cfa7469ce8b40226a74e480d01bf8c52b23..2af7f4a1828a96c4de9058ad6ea8362172560c00 100644 (file)
--- a/matita/matita/lib/extraction.ma
+++ b/matita/matita/lib/extraction.ma
@@ -186,4 +186,23 @@ axiom lt: nat → nat → Prop.
 (*BUG: elimination principles not extracted *)
 inductive myvect (A: Type[0]) (b:nat) : nat → Type[0] ≝
    myemptyv : myvect A b O
- | mycons: ∀n. lt n b → A → myvect A b n → myvect A b (S n).
\ No newline at end of file
+ | mycons: ∀n. lt n b → A → myvect A b n → myvect A b (S n).
+ 
+inductive False: Prop ≝ .
+
+inductive Empty: Type[0] ≝ .
+
+inductive bool: Type[0] ≝ true: bool | false:bool.
+
+inductive eq (A:Type[1]) (a:A) : A → Prop ≝ refl: eq A a a.
+
+(* BUG: requires coercion *)
+definition cast_bug1 ≝
+ λH:eq Type[0] bool nat. S (match H return λA:Type[0].λ_.A with [ refl ⇒ true ]).
+
+(* BUG: requires top type *)
+definition cast_bug2 ≝
+ λb.
+  match true return λb.match b with [ true ⇒ nat → nat | false ⇒ bool ] with
+   [ true ⇒ S | false ⇒ false ]
+  O. 
\ No newline at end of file