aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2393.v
blob: fb4f92619f7b303673d3c4eb37513a972a4219c1 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
Require Import Program.

Inductive T := MkT.

Definition sizeOf (t : T) : nat
    := match t with
       | MkT => 1
       end.
Variable vect : nat -> Type.
Program Fixpoint idType (t : T) (n := sizeOf t) (b : vect n) {measure n} : T
    := match t with
       | MkT => MkT
       end.