blob: 83a581338f358bb09d410a8e8bb3ecff3686522a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
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)).
Module LocalDefUnfolding.
Unset Printing Projections.
Record U A (B:=A) C := {c:B*A*C;a:=(A,B,C,c);b:a=a}.
Print a.
Print b.
End LocalDefUnfolding.
|
