blob: 6a559e75c3995e34832495b335427f5403b72f3a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
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.
Require Import Wf_nat.
Solve Obligations using auto with arith.
|
