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/bugs/opened/3490.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/opened/3490.v')
-rw-r--r-- | test-suite/bugs/opened/3490.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3490.v b/test-suite/bugs/opened/3490.v new file mode 100644 index 00000000..e7a5caa1 --- /dev/null +++ b/test-suite/bugs/opened/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. |