diff options
Diffstat (limited to 'test-suite/output/Notations3.out')
-rw-r--r-- | test-suite/output/Notations3.out | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 304353f55..996af5927 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -231,3 +231,13 @@ fun l : list nat => match l with : list nat -> list nat Argument scope is [list_scope] +Notation +"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope +(default interpretation) +"'exists' ! x .. y , p" := ex + (unique + (fun x => .. (ex (unique (fun y => p))) ..)) +: type_scope (default interpretation) +Notation +"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope +(default interpretation) |