blob: 14d63d39c4e7a044c9dc97ea1b044464d083684b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Set Printing Projections.
Set Primitive Projections.
Class HostFunction := host_func : Type.
Section store.
Context `{HostFunction}.
Record store := { store_funcs : host_func }.
End store.
Check (fun (S:@store nat) => S.(store_funcs)).
|
