diff options
| -rw-r--r-- | test-suite/output/Notations4.out | 8 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 16 |
2 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index acd69f3f50..2ff21f6a57 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -23,3 +23,11 @@ Let "x" e1 e2 : expr fun x : nat => (# x)%nat : nat -> nat +fun x : nat => ## x + : nat -> nat +fun x : nat => # x + : nat -> nat +fun x : nat => ### x + : nat -> nat +fun x : nat => ## x + : nat -> nat 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. |