From 764a1d9f5127b30d0f20b062f04645fa0d2a53c8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Feb 2022 15:47:12 -0800 Subject: [PATCH] chore: fix tests --- tests/lean/StxQuot.lean.expected.out | 4 ++-- tests/lean/match1.lean.expected.out | 2 +- tests/lean/match2.lean | 4 ++-- tests/lean/match2.lean.expected.out | 2 +- tests/lean/ppMotives.lean.expected.out | 4 ++-- tests/lean/unusedLet.lean.expected.out | 2 +- 6 files changed, 9 insertions(+), 9 deletions(-) diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index 59f133038e..59d8dffd40 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -36,8 +36,8 @@ StxQuot.lean:18:15: error: expected term "(Term.structInst\n \"{\"\n []\n [(group\n (Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)\n [])]\n (Term.optEllipsis [])\n []\n \"}\")" "(Command.section \"section\" [])" "(Command.section \"section\" [`foo._@.UnhygienicMain._hyg.1])" -"(Term.match\n \"match\"\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))" -"(Term.match\n \"match\"\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))" +"(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))" +"(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))" "#[`a._@.UnhygienicMain._hyg.1, `b._@.UnhygienicMain._hyg.1]" "1" "(Term.sufficesDecl [] `x._@.UnhygienicMain._hyg.1 (Term.fromTerm \"from\" `x._@.UnhygienicMain._hyg.1))" diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out index e3aa811452..0adbb091df 100644 --- a/tests/lean/match1.lean.expected.out +++ b/tests/lean/match1.lean.expected.out @@ -36,7 +36,7 @@ fun x x_1 => | some a, some b => some (a + b) | x, x_2 => none : Option Nat → Option Nat → Option Nat fun x => - (match x : Nat → Nat → Nat with + (match (motive := Nat → Nat → Nat) x with | 0 => id | Nat.succ x => id) x : Nat → Nat diff --git a/tests/lean/match2.lean b/tests/lean/match2.lean index 34117a680c..66067cc6cd 100644 --- a/tests/lean/match2.lean +++ b/tests/lean/match2.lean @@ -80,11 +80,11 @@ match b, x with | b, x => false def h6' {b : Bool} (x : Foo b) : Bool := -match (generalizing := true) b, x : (b : Bool) → Foo b → Bool with +match (generalizing := true) (motive := (b : Bool) → Foo b → Bool) b, x with | _, Foo.bar => true | b, x => false def h6'' {b : Bool} (x : Foo b) : Bool := -match (generalizing := false) b, x : (b : Bool) → Foo b → Bool with +match (generalizing := false) (motive := (b : Bool) → Foo b → Bool) b, x with | _, Foo.bar => true | b, x => false diff --git a/tests/lean/match2.lean.expected.out b/tests/lean/match2.lean.expected.out index 98a2e17f59..0c3b35f693 100644 --- a/tests/lean/match2.lean.expected.out +++ b/tests/lean/match2.lean.expected.out @@ -15,4 +15,4 @@ true false false ---- Foo 3 -match2.lean:83:0-85:21: error: the '(generalizing := true)' parameter is not supported when the 'match' type is explicitly provided +match2.lean:83:0-85:21: error: the '(generalizing := true)' parameter is not supported when the 'match' motive is explicitly provided diff --git a/tests/lean/ppMotives.lean.expected.out b/tests/lean/ppMotives.lean.expected.out index 90f1f6480d..506e4c010c 100644 --- a/tests/lean/ppMotives.lean.expected.out +++ b/tests/lean/ppMotives.lean.expected.out @@ -11,7 +11,7 @@ protected def Nat.add : Nat → Nat → Nat := fun x x_1 => Nat.brecOn (motive := fun x => Nat → Nat) x_1 (fun x f x_2 => - (match x_2, x : (x x : Nat) → Nat.below (motive := fun x => Nat → Nat) x → Nat with + (match (motive := (x x : Nat) → Nat.below (motive := fun x => Nat → Nat) x → Nat) x_2, x with | a, Nat.zero => fun x => a | a, Nat.succ b => fun x => Nat.succ (PProd.fst x.fst a)) f) @@ -22,7 +22,7 @@ fun x x_1 x_2 x_3 => | α, .(α), Eq.refl α, a => HEq.refl a theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), HEq (cast h a) a := fun x x_1 x_2 x_3 => - match x, x_1, x_2, x_3 : ∀ (x x_4 : Sort u) (x_5 : x = x_4) (x_6 : x), HEq (cast x_5 x_6) x_6 with + match (motive := ∀ (x x_4 : Sort u) (x_5 : x = x_4) (x_6 : x), HEq (cast x_5 x_6) x_6) x, x_1, x_2, x_3 with | α, .(α), Eq.refl α, a => HEq.refl a def fact : Nat → Nat := fun n => Nat.recOn n 1 fun n acc => (n + 1) * acc diff --git a/tests/lean/unusedLet.lean.expected.out b/tests/lean/unusedLet.lean.expected.out index 009bb5cf05..e282187113 100644 --- a/tests/lean/unusedLet.lean.expected.out +++ b/tests/lean/unusedLet.lean.expected.out @@ -4,7 +4,7 @@ false def f : Nat → Nat := fun x => Nat.brecOn x fun x f => - (match x : (x : Nat) → Nat.below x → Nat with + (match (motive := (x : Nat) → Nat.below x → Nat) x with | 0 => fun x => 1 | Nat.succ n => fun x => let y := 42;