From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- test-suite/bugs/closed/3490.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 test-suite/bugs/closed/3490.v (limited to 'test-suite/bugs/closed/3490.v') diff --git a/test-suite/bugs/closed/3490.v b/test-suite/bugs/closed/3490.v new file mode 100644 index 00000000..e7a5caa1 --- /dev/null +++ b/test-suite/bugs/closed/3490.v @@ -0,0 +1,27 @@ +Inductive T : Type := +| Var : nat -> T +| Arr : T -> T -> T. + +Inductive Tele : list T -> Type := +| Tnil : @Tele nil +| Tcons : forall ls, forall (t : @Tele ls) (l : T), @Tele (l :: ls). + +Fail Fixpoint TeleD (ls : list T) (t : Tele ls) {struct t} + : { x : Type & x -> nat -> Type } := + match t return { x : Type & x -> nat -> Type } with + | Tnil => @existT Type (fun x => x -> nat -> Type) unit (fun (_ : unit) (_ : nat) => unit) + | Tcons ls t' l => + let (result, get) := TeleD ls t' in + @existT Type (fun x => x -> nat -> Type) + { v : result & (fix TD (t : T) {struct t} := + match t with + | Var n => + get v n + | Arr a b => TD a -> TD b + end) l } + (fun x n => + match n return Type with + | 0 => projT2 x + | S n => get (projT1 x) n + end) + end. -- cgit v1.2.3