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.
|
