blob: 0464c62c099236fbbec6c60d39b23f3c27fdd917 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(* Example from #9521 *)
Module A.
Declare Custom Entry expr.
Notation "expr0:( s )" := s (s custom expr at level 0).
Notation "#" := 0 (in custom expr at level 1).
Check expr0:(#). (* Should not be an anomaly "unknown level 0" *)
End A.
(* Another example from a comment at #11561 *)
Module B.
Declare Custom Entry special.
Declare Custom Entry expr.
Notation "## x" := (S x) (in custom expr at level 10, x custom special at level 10).
Notation "[ e ]" := e (e custom expr at level 10).
Notation "1" := 1 (in custom special).
Check [ ## 1 ].
End B.
|
