diff options
Diffstat (limited to 'test-suite/output/Notations4.out')
| -rw-r--r-- | test-suite/output/Notations4.out | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index f65696e464..e121b5e86c 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -71,3 +71,39 @@ The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". +Entry constr:expr is +[ "201" RIGHTA + [ "{"; constr:operconstr LEVEL "200"; "}" ] ] + +fun x : nat => [ x ] + : nat -> nat +fun x : nat => [x] + : nat -> nat +∀ x : nat, x = x + : Prop +File "stdin", line 219, characters 0-160: +Warning: Notation "∀ _ .. _ , _" was already defined with a different format +in scope type_scope. [notation-incompatible-format,parsing] +∀x : nat,x = x + : Prop +File "stdin", line 232, characters 0-60: +Warning: Notation "_ %%% _" was already defined with a different format. +[notation-incompatible-format,parsing] +File "stdin", line 236, characters 0-64: +Warning: Notation "_ %%% _" was already defined with a different format. +[notation-incompatible-format,parsing] +File "stdin", line 241, characters 0-62: +Warning: Lonely notation "_ %%%% _" was already defined with a different +format. [notation-incompatible-format,parsing] +3 %% 4 + : nat +3 %% 4 + : nat +3 %% 4 + : nat +File "stdin", line 269, characters 0-61: +Warning: The format modifier is irrelevant for only parsing rules. +[irrelevant-format-only-parsing,parsing] +File "stdin", line 273, characters 0-63: +Warning: The only parsing modifier has no effect in Reserved Notation. +[irrelevant-reserved-notation-only-parsing,parsing] |