1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Declare Custom Entry example.
Module M1.
Fixpoint stupid (x : nat) : nat := 1.
Reserved Notation " x '==' 1 " (in custom example at level 0, x constr).
Notation " x '==' 1" := (stupid x) (in custom example).
End M1.
Module M2.
Fixpoint stupid (x : nat) : nat := 1.
Notation " x '==' 1" := (stupid x) (in custom example at level 0).
Fail Notation " x '==' 1" := (stupid x) (in custom example at level 1).
End M2.
Module M3.
Reserved Notation " x '==' 1 " (in custom example at level 55, x constr).
Fixpoint stupid (x : nat) : nat := 1
where " x '==' 1" := (stupid x) (in custom example).
End M3.
|
