blob: 40ca39e38a70ee31ecb575a4c932b2471daa967e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* Adding an only-printing notation should not override existing
interpretations for the same notation. *)
Notation "$ x" := (@id nat x) (only parsing, at level 0).
Notation "$ x" := (@id bool x) (only printing, at level 0).
Check $1. (* Was: Error: Unknown interpretation for notation "$ _". *)
(* Adding an only-printing notation should not let believe
that a parsing rule has been given *)
Notation "$ x" := (@id bool x) (only printing, at level 0).
Notation "$ x" := (@id nat x) (only parsing, at level 0).
Check $1. (* Was: Error: Syntax Error: Lexer: Undefined token *)
|
