diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations3.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 180e8d337e..421ec987ff 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -183,9 +183,13 @@ Check letpair x [1] = {0}; return (1,2,3,4). (* Test spacing in #5569 *) +Section S1. +Variable plus : nat -> nat -> nat. +Infix "+" := plus. Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. +End S1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). |