blob: dd981279dbd7bdb229fe2f62c8cfe5c1e82a37c7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Require Extraction.
Inductive t (sig: list nat) :=
| T (k: nat).
Record pkg :=
{ _sig: list nat;
_t : t _sig }.
Definition map (f: nat -> nat) (p: pkg) :=
{| _sig := p.(_sig);
_t := match p.(_t) with
| T _ k => T p.(_sig) (f k)
end |}.
Extraction Implicit Build_pkg [_sig].
Extraction TestCompile map.
|
