Points-fixes avec let-in

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5722 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 30 insertions, 0 deletions

diff --git a/test-suite/success/Fixpoint.v8 b/test-suite/success/Fixpoint.v8
new file mode 100644
index 0000000000..292366242c
--- /dev/null
+++ b/test-suite/success/Fixpoint.v8
@@ -0,0 +1,30 @@
+(* Playing with (co-)fixpoints with local definitions *)
+
+Inductive listn : nat -> Set :=
+  niln : listn 0
+| consn : forall n:nat, nat -> listn n -> listn (S n).
+
+Fixpoint f (n:nat) (m:=pred n) (l:listn m) (p:=S n) {struct l} : nat :=
+   match n with O => p | _ => 
+     match l with niln => p | consn q _ l => f (S q) l end
+   end.
+
+Eval compute in (f 2 (consn 0 0 niln)).
+
+CoInductive Stream : nat -> Set :=
+  Consn : forall n, nat -> Stream n -> Stream (S n).
+
+CoFixpoint g (n:nat) (m:=pred n) (l:Stream m) (p:=S n) : Stream p :=
+    match n return (let m:=pred n in forall l:Stream m, let p:=S n in Stream p)
+    with
+    | O => fun l:Stream 0 => Consn O 0 l
+    | S n' =>
+      fun l:Stream n' =>
+      let l' :=
+        match l in Stream q return Stream (pred q) with Consn _ _ l => l end
+      in
+      let a := match l with Consn _ a l => a end in
+      Consn (S n') (S a) (g n' l')
+   end l.
+
+Eval compute in (fun l => match g 2 (Consn 0 6 l) with Consn _ a _ => a end).