From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- test-suite/success/Fixpoint.v | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 test-suite/success/Fixpoint.v (limited to 'test-suite/success/Fixpoint.v') diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v new file mode 100644 index 00000000..680046da --- /dev/null +++ b/test-suite/success/Fixpoint.v @@ -0,0 +1,31 @@ +(* 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). + -- cgit v1.2.3