test-suite/bugs/closed/2393.v


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.