From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/success/Case20.v | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 test-suite/success/Case20.v (limited to 'test-suite/success/Case20.v') diff --git a/test-suite/success/Case20.v b/test-suite/success/Case20.v new file mode 100644 index 00000000..67eebf72 --- /dev/null +++ b/test-suite/success/Case20.v @@ -0,0 +1,35 @@ +(* Example taken from RelationAlgebra *) +(* Was failing from r16205 up to now *) + +Require Import BinNums. + +Section A. + +Context (A:Type) {X: A} (tst:A->Type) (top:forall X, X). + +Inductive v: (positive -> A) -> Type := +| v_L: forall f', v f' +| v_N: forall f', + v (fun n => f' (xO n)) -> + (positive -> tst (f' xH)) -> + v (fun n => f' (xI n)) -> v f'. + +Fixpoint v_add f' (t: v f') n: (positive -> tst (f' n)) -> v f' := + match t in (v o) return ((positive -> (tst (o n))) -> v o) with + | v_L f' => + match n return ((positive -> (tst (f' n))) -> v f') with + | xH => fun x => v_N _ (v_L _) x (v_L _) + | xO n => fun x => v_N _ + (v_add (fun n => f' (xO n)) (v_L _) n x) (fun _ => top _) (v_L _) + | xI n => fun x => v_N _ + (v_L _) (fun _ => top _) (v_add (fun n => f' (xI n)) (v_L _) n x) + end + | v_N f' l y r => + match n with + | xH => fun x => v_N _ l x r + | xO n => fun x => v_N _ (v_add (fun n => f' (xO n)) l n x) y r + | xI n => fun x => v_N _ l y (v_add (fun n => f' (xI n)) r n x) + end + end. + +End A. -- cgit v1.2.3