diff options
| -rw-r--r-- | test-suite/output/Notations.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations.v | 11 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 321c60eb10..3ab3de4571 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -18,3 +18,7 @@ forall n : nat, n = 0 : Z 3 + 3 : znat +[1; 2; 4] + : list nat +(1; 2, 4) + : nat * nat * nat diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index fdce2b2511..4382975e86 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -55,3 +55,14 @@ Notation "z1 + z2" := (addz z1 z2) : znat_scope. only tested with coercion still present *) Check (3+3). + +(**********************************************************************) +(* Check recursive notations *) + +Require Import List. +Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). +Check [1;2;4]. + +Reserved Notation "( x ; y , .. , z )" (at level 0). +Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z). +Check (1;2,4). |