diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations2.out | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations2.v | 10 |
2 files changed, 14 insertions, 2 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index c1a7e961a..20d20d826 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -4,3 +4,9 @@ : nat forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x : Prop +match (0, 0, 0) with +| (x, y, z) => x + y + z +end + : nat +let '(a, _, _) := (2, 3, 4) in a + : nat diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 3eeff401c..2e136edf1 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -10,11 +10,17 @@ Check (2 3). (* (were not working from revision 11886 to 12951) *) Record Binop := { binop :> nat -> nat -> nat }. -Class Plusop := { plusop : Binop; z : nat }. +Class Plusop := { plusop : Binop; zero : nat }. Infix "[+]" := plusop (at level 40). -Instance Plus : Plusop := {| plusop := {| binop := plus |} ; z := 0 |}. +Instance Plus : Plusop := {| plusop := {| binop := plus |} ; zero := 0 |}. Check 2[+]3. (* Test bug #2091 (variable le was printed using <= !) *) Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x. + +(* Test recursive notations in cases pattern *) + +Remove Printing Let prod. +Check match (0,0,0) with (x,y,z) => x+y+z end. +Check let '(a,b,c) := ((2,3),4) in a. |