blob: 098a518dc4ed0542ab8b8e9347471697789c79a8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Set Printing 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)).
|