From 08e17790d0aebf97638fc12bcb4ae3d837db76ea Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 2 Aug 2012 16:37:41 +0000 Subject: [PATCH] ... --- matita/matita/lib/extraction.ma | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/matita/matita/lib/extraction.ma b/matita/matita/lib/extraction.ma index 35a9a5788..8e46509fa 100644 --- a/matita/matita/lib/extraction.ma +++ b/matita/matita/lib/extraction.ma @@ -120,7 +120,31 @@ definition ttest11_aux ≝ λS:Type[1]. S → Nat. definition ttest11 ≝ λf:ttest11_aux True. f I. -(*BUG here: requires F_omega eat_args*) definition ttest12 ≝ λf:True → Nat. f I. (*GENERAL BUG: name clashes when binders shadow each other in CIC*) + +(*BUG: mutual type definitions not handled correctly: the ref is computed in a + wrong way *) + +(*BUG: multiple let-reced things are given the same (wrong) name*) + +(*BUG: for OCaml: cofixpoint not distinguished from fixpoints*) + +let rec rtest1 (n:nat) : nat ≝ + match n with + [ O ⇒ O + | S m ⇒ rtest1 m ]. + +let rec f (n:nat) : nat ≝ + match n with + [ O ⇒ O + | S m ⇒ g m ] +and g (n:nat) : nat ≝ + match n with + [ O ⇒ O + | S m ⇒ f m ]. + +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 -- 2.39.2