diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/success/Case20.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/success/Case20.v')
-rw-r--r-- | test-suite/success/Case20.v | 35 |
1 files changed, 35 insertions, 0 deletions
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. |