diff options
Diffstat (limited to 'test-suite/output/Notations.v')
| -rw-r--r-- | test-suite/output/Notations.v | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 612b5325..adba688e 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -68,7 +68,7 @@ Coercion Zpos: nat >-> znat. Delimit Scope znat_scope with znat. Open Scope znat_scope. -Variable addz : znat -> znat -> znat. +Parameter addz : znat -> znat -> znat. Notation "z1 + z2" := (addz z1 z2) : znat_scope. (* Check that "3+3", where 3 is in nat and the coercion to znat is implicit, @@ -133,7 +133,8 @@ Fail Notation "( x , y , .. , z )" := (pair x (pair y z)). Fail Notation "( x , y , .. , z )" := (pair x .. (pair y w) ..). (* Right-unbound variable *) -Fail Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..). +(* Now allowed with an only parsing restriction *) +Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..). (* Not the right kind of recursive pattern *) Fail Notation "( x , y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..)). @@ -244,7 +245,11 @@ Check (fun x => match x with SOME2 x => x | NONE2 => 0 end). Notation NONE3 := @None. Notation SOME3 := @Some. -Check (fun x => match x with SOME3 x => x | NONE3 => 0 end). +Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end). + +Notation "a :'" := (cons a) (at level 12). + +Check (fun x => match x with | nil => NONE | h :' t => SOME3 _ t end). (* Check correct matching of "Type" in notations. Of course the notation denotes a term that will be reinterpreted with a different @@ -275,3 +280,4 @@ Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p. Notation "1" := eq_refl. Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p. + |