blob: 35f36e87d7607fb568e1dbc1415a3e794d9053f5 (
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}.
#[universes(template)] Record store := { store_funcs : host_func }.
End store.
Check (fun (S:@store nat) => S.(store_funcs)).
|
