diff options
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/Notations.out | 4 | ||||
-rw-r--r-- | test-suite/output/Notations.v | 16 |
2 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 2066a7ef3..6c69c097d 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -50,3 +50,7 @@ Nil : forall A : Type, list A NIL:list nat : list nat +[|1, 2, 3; 4, 5, 6|] + : Z * Z * Z * (Z * Z * Z) +fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z + : (Z -> Z -> Z -> Z) -> Z diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 6e637aca3..f19ba998f 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -129,3 +129,19 @@ Check Nil. Notation NIL := nil. Check NIL : list nat. + +(**********************************************************************) +(* Check notations with several recursive patterns *) + +Notation "[| x , y , .. , z ; a , b , .. , c |]" := + (pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)). +Check [|1,2,3;4,5,6|]. + +(**********************************************************************) +(* Test recursive notations involving applications *) +(* Caveat: does not work for applied constant because constants are *) +(* classified as notations for the particular constant while this *) +(* generic application notation is classified as generic *) + +Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y). +Check fun f => {| f; 0; 1; 2 |} : Z. |