diff options
Diffstat (limited to 'test-suite/output/Notations4.v')
| -rw-r--r-- | test-suite/output/Notations4.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 12e98c3d64..4720cb0561 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -106,3 +106,19 @@ Notation "# x" := (Some x). Check fun x => (# x)%nat. End E. + +(* Other tests of precedence *) + +Module F. + +Notation "# x" := (S x) (at level 20) : nat_scope. +Notation "## x" := (S x) (at level 20). +Check fun x => S x. +Open Scope nat_scope. +Check fun x => S x. +Notation "### x" := (S x) (at level 20) : nat_scope. +Check fun x => S x. +Close Scope nat_scope. +Check fun x => S x. + +End F. |