diff options
| author | Hugo Herbelin | 2018-09-25 12:53:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | c90e2d81ee0dc5198176300f0140a9e0a71a4cc5 (patch) | |
| tree | 873804b3f934f27896b534f7b73e63ea462e2ac1 | |
| parent | 9bc339f529fc2ee2389a717914514829a73686bc (diff) | |
Using scope for printing: more tests.
| -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. |