diff options
| -rw-r--r-- | test-suite/output/Notations3.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 6 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index c66f80122..e5dbfcb4b 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -120,3 +120,5 @@ where letpair x [1] = {0}; return (1, 2, 3, 4) : nat * nat * nat * nat +{{ 1 | 1 // 1 }} + : nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 58f9e15ab..b1015137d 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -180,3 +180,9 @@ Reserved Notation "'letpair' x [1] = { A } ; 'return' ( b0 , b1 , .. , b2 )" Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" := (let x:=a in ( .. (b0,b1) .., b2)). Check letpair x [1] = {0}; return (1,2,3,4). + +(* Test spacing in #5569 *) + +Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) + (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). +Check 1+1+1. |