1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
Module A.
Set Primitive Projections.
Record foo := Foo { foo_n : nat }.
Notation "'■' x" := (foo_n x) (at level 50).
Check forall (f:foo), ■ f = ■ f.
End A.
Module A'.
Set Primitive Projections.
Record foo := Foo { foo_n : nat }.
Notation "'■' x" := x.(foo_n) (at level 50).
Check forall (f:foo), ■ f = ■ f.
End A'.
(* Variant with non-primitive projections *)
Module B.
Record T := {a:nat}.
Notation "%% x" := (a x) (at level 0, x at level 0).
Check fun x => %%x.
End B.
Module B'.
Record T := {a:nat}.
Notation "%% x" := x.(a) (at level 0, x at level 0).
Check fun x => %%x.
End B'.
|
