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