]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/extraction.ma
Preliminary work on (co)inductive types.
[helm.git] / matita / matita / lib / extraction.ma
index 8e46509fa9696eff17821b5def068ddafb993ba4..5d02b5760dad18ed5165707f686cb715e044ac45 100644 (file)
@@ -145,6 +145,41 @@ and g (n:nat) : nat ≝
  [ O ⇒ O
  | S m ⇒ f m ].
 
+(*BUG: pattern matching patterns when arguments have been deleted from
+  the constructor are wrong *)
+
+(*BUG: constructor names in pattern should be capitalised correctly;
+  name clashes must be avoided*)
+
 coinductive stream: Type[0] ≝ scons : nat → stream → stream.
 
-let corec div (n:nat) : stream ≝ scons n (div (S n)).
\ No newline at end of file
+let corec div (n:nat) : stream ≝ scons n (div (S n)).
+
+definition rtest2 : nat → stream → nat ≝
+ λm,s. match s with [ scons n l ⇒ m + n ].
+
+(*
+let rec mkterm (n:nat) : nat ≝
+ match n with
+ [ O ⇒ O
+ | S m ⇒ mkterm m ]
+and mktyp (n:nat) : Type[0] ≝
+ match n with
+ [ O ⇒ nat
+ | S m ⇒ mktyp m ].*)
+
+inductive mynat : Type[0] ≝ myzero: mynat | mysucc: mynat → mynat.
+
+(*FEATURE: print kind signatures*)
+inductive T1 : (Type[0] → Type[0]) → ∀B:Type[0]. mynat → Type[0] → Type[0] ≝ .
+
+(*Not in F_omega *)
+inductive T2 : (Type[0] → Type[0]) → ∀B:Type[0]. B → Type[0] → Type[0] ≝ .
+
+(* no content *)
+inductive T3 : (Type[0] → Type[0]) → CProp[2] ≝ .
+
+(*BUG: elimination principles not extracted *)
+inductive myvect (A: Type[0]) (b:nat) : nat → Type[0] ≝
+   myemptyv : myvect A b 0
+ | mycons: ∀n. n < b → A → myvect A b n → myvect A b (S n).
\ No newline at end of file