diff options
Diffstat (limited to 'test-suite/output/Notations2.v')
| -rw-r--r-- | test-suite/output/Notations2.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 531398bb0..923caedac 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -36,8 +36,9 @@ Check fun P:nat->nat->Prop => fun x:nat => ex (P x). (* Test notations with binders *) -Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) - (x binder, y binder, at level 200, right associativity). +Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) + (x binder, y binder, at level 200, right associativity, + format "'[ ' ∃ x .. y ']' , P"). Check (∃ n p, n+p=0). |