diff options
| author | Hugo Herbelin | 2018-10-15 15:50:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | 8f7c82b8a67a3c94073e55289996f02285c04914 (patch) | |
| tree | e219713f3408297c18da63186f40bb0b8ab0360e /test-suite | |
| parent | e2c4d3ad72b85f1fb1ea1a7c42aff0831eff3c30 (diff) | |
Printing priority to most recent notation in case of non-open scopes with delim.
This modifies the strategy in previous commits so that priorities are
as before in case of non-open scopes with delimiters.
Additionally, we document the rare situation of overlapping
applicative notations (maybe this is too rare and ad hoc to be worth
being documented though).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 14 |
2 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 2ff21f6a57..40d875e8ab 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -31,3 +31,5 @@ fun x : nat => ### x : nat -> nat fun x : nat => ## x : nat -> nat +fun x : nat => (x.-1)%pred + : nat -> nat diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4720cb0561..4196c7e6b4 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -122,3 +122,17 @@ Close Scope nat_scope. Check fun x => S x. End F. + +(* Lower priority of generic application rules *) + +Module G. + +Declare Scope predecessor_scope. +Delimit Scope predecessor_scope with pred. +Declare Scope app_scope. +Delimit Scope app_scope with app. +Notation "x .-1" := (Nat.pred x) (at level 10, format "x .-1") : predecessor_scope. +Notation "f ( x )" := (f x) (at level 10, format "f ( x )") : app_scope. +Check fun x => pred x. + +End G. |