From 7627458aac7712abd42dd4eec857d2b21269657e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Mar 2021 15:10:50 -0800 Subject: [PATCH] chore: fix tests We are not using the `!` suffix anymore for keywords. --- tests/lean/isDefEqOffsetBug.lean | 2 +- tests/lean/run/326.lean | 2 +- tests/lean/run/KyleAlg.lean | 4 ++-- tests/lean/run/alg.lean | 2 +- tests/lean/run/balg.lean | 4 ++-- tests/lean/run/expandAbbrevAtIsClass.lean | 4 ++-- tests/lean/run/matrix.lean | 8 ++++---- tests/lean/run/newfrontend1.lean | 12 ++++++------ tests/lean/run/ofNatNormNum.lean | 4 ++-- tests/lean/run/offsetIssue.lean | 2 +- 10 files changed, 22 insertions(+), 22 deletions(-) diff --git a/tests/lean/isDefEqOffsetBug.lean b/tests/lean/isDefEqOffsetBug.lean index bb0bde7262..d03230dc24 100644 --- a/tests/lean/isDefEqOffsetBug.lean +++ b/tests/lean/isDefEqOffsetBug.lean @@ -3,7 +3,7 @@ class Zero (α : Type u) where export Zero (zero) -instance [Zero α] : OfNat α (natLit! 0) where +instance [Zero α] : OfNat α (nat_lit 0) where ofNat := zero class AddGroup (α : Type u) extends Add α, Zero α, Neg α where diff --git a/tests/lean/run/326.lean b/tests/lean/run/326.lean index f944f1d0f8..081f1b7e2e 100644 --- a/tests/lean/run/326.lean +++ b/tests/lean/run/326.lean @@ -1,4 +1,4 @@ -abbrev Zero α := OfNat α (natLit! 0) +abbrev Zero α := OfNat α (nat_lit 0) class Monoid (α : Type u) [Zero α] extends Add α where zero_add (a : α) : 0 + a = a diff --git a/tests/lean/run/KyleAlg.lean b/tests/lean/run/KyleAlg.lean index 4d1fab7666..f29be419fd 100644 --- a/tests/lean/run/KyleAlg.lean +++ b/tests/lean/run/KyleAlg.lean @@ -18,14 +18,14 @@ class One (α : Type u) where one : α export One (one) -instance [One α] : OfNat α (natLit! 1) where +instance [One α] : OfNat α (nat_lit 1) where ofNat := one class Zero (α : Type u) where zero : α export Zero (zero) -instance [Zero α] : OfNat α (natLit! 0) where +instance [Zero α] : OfNat α (nat_lit 0) where ofNat := zero class MulComm (α : Type u) [Mul α] : Prop where diff --git a/tests/lean/run/alg.lean b/tests/lean/run/alg.lean index 903866a6a4..1ef85d2f37 100644 --- a/tests/lean/run/alg.lean +++ b/tests/lean/run/alg.lean @@ -17,7 +17,7 @@ instance [CommSemigroup α] : MulComm α where class One (α : Type u) where one : α -instance [One α] : OfNat α (natLit! 1) where +instance [One α] : OfNat α (nat_lit 1) where ofNat := One.one class Monoid (α : Type u) extends Semigroup α, One α where diff --git a/tests/lean/run/balg.lean b/tests/lean/run/balg.lean index 0110088893..20efabee49 100644 --- a/tests/lean/run/balg.lean +++ b/tests/lean/run/balg.lean @@ -56,10 +56,10 @@ abbrev inv {G : Group} (a : G) : G := postfix:max "⁻¹" => inv -instance (G : Group) : OfNat (coeSort G.toMagma) (natLit! 1) where +instance (G : Group) : OfNat (coeSort G.toMagma) (nat_lit 1) where ofNat := G.one -instance (G : Group) : OfNat (G.toMagma.α) (natLit! 1) where +instance (G : Group) : OfNat (G.toMagma.α) (nat_lit 1) where ofNat := G.one structure CommGroup extends Group where diff --git a/tests/lean/run/expandAbbrevAtIsClass.lean b/tests/lean/run/expandAbbrevAtIsClass.lean index 575c392131..953f432fb0 100644 --- a/tests/lean/run/expandAbbrevAtIsClass.lean +++ b/tests/lean/run/expandAbbrevAtIsClass.lean @@ -1,6 +1,6 @@ -def one (α : Type u) [OfNat α (natLit! 1)] : α := 1 +def one (α : Type u) [OfNat α (nat_lit 1)] : α := 1 -abbrev HasOne (α : Type u) := OfNat α (natLit! 1) +abbrev HasOne (α : Type u) := OfNat α (nat_lit 1) def one' (α : Type u) [HasOne α] : α := 1 diff --git a/tests/lean/run/matrix.lean b/tests/lean/run/matrix.lean index 70779d4893..e2d6882949 100644 --- a/tests/lean/run/matrix.lean +++ b/tests/lean/run/matrix.lean @@ -4,19 +4,19 @@ Helper classes for Lean 3 users class One (α : Type u) where one : α -instance [OfNat α (natLit! 1)] : One α where +instance [OfNat α (nat_lit 1)] : One α where one := 1 -instance [One α] : OfNat α (natLit! 1) where +instance [One α] : OfNat α (nat_lit 1) where ofNat := One.one class Zero (α : Type u) where zero : α -instance [OfNat α (natLit! 0)] : Zero α where +instance [OfNat α (nat_lit 0)] : Zero α where zero := 0 -instance [Zero α] : OfNat α (natLit! 0) where +instance [Zero α] : OfNat α (nat_lit 0) where ofNat := Zero.zero /- Simple Matrix -/ diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean index a07f7bef3c..2246eb2829 100644 --- a/tests/lean/run/newfrontend1.lean +++ b/tests/lean/run/newfrontend1.lean @@ -94,7 +94,7 @@ by { theorem simple7 (x y z : Nat) : y = z → x = x → x = y → x = z := by { intro h1; intro _; intro h3; - refine! Eq.trans ?pre ?post; + refine' Eq.trans ?pre ?post; exact y; { exact h3 } { exact h1 } @@ -102,7 +102,7 @@ by { theorem simple8 (x y z : Nat) : y = z → x = x → x = y → x = z := by intro h1; intro _; intro h3 -refine! Eq.trans ?pre ?post +refine' Eq.trans ?pre ?post case post => exact h1 case pre => exact h3 @@ -110,7 +110,7 @@ theorem simple9 (x y z : Nat) : y = z → x = x → x = y → x = z := by intros h1 _ h3 traceState focus - refine! Eq.trans ?pre ?post + refine' Eq.trans ?pre ?post first | exact h1 assumption @@ -122,7 +122,7 @@ theorem simple9b (x y z : Nat) : y = z → x = x → x = y → x = z := by intros h1 _ h3 traceState focus - refine! Eq.trans ?pre ?post + refine' Eq.trans ?pre ?post first | exact h1 | exact y; exact h3 @@ -132,12 +132,12 @@ theorem simple9c (x y z : Nat) : y = z → x = x → x = y → x = z := by intros h1 _ h3 solve | exact h1 - | refine! Eq.trans ?pre ?post; exact y; exact h3; assumption + | refine' Eq.trans ?pre ?post; exact y; exact h3; assumption | exact h3 theorem simple9d (x y z : Nat) : y = z → x = x → x = y → x = z := by intros h1 _ h3 - refine! Eq.trans ?pre ?post + refine' Eq.trans ?pre ?post solve | exact h1 | exact y diff --git a/tests/lean/run/ofNatNormNum.lean b/tests/lean/run/ofNatNormNum.lean index 6b9ac6a7ec..d54b03f812 100644 --- a/tests/lean/run/ofNatNormNum.lean +++ b/tests/lean/run/ofNatNormNum.lean @@ -12,10 +12,10 @@ class Zero (α : Type u) where class One (α : Type u) where one : α -instance [Zero α] : OfNat α (natLit! 0) where +instance [Zero α] : OfNat α (nat_lit 0) where ofNat := Zero.zero -instance [One α] : OfNat α (natLit! 1) where +instance [One α] : OfNat α (nat_lit 1) where ofNat := One.one -- Some example structure diff --git a/tests/lean/run/offsetIssue.lean b/tests/lean/run/offsetIssue.lean index 0a1028ef9d..7bbc89a73d 100644 --- a/tests/lean/run/offsetIssue.lean +++ b/tests/lean/run/offsetIssue.lean @@ -3,7 +3,7 @@ def BV (n : Nat) := { a : Array Bool // a.size = n } axiom foo {n m : Nat} (a : BV n) (b : BV m) : BV (n - m) def test (x1 : BV 30002) (x2 : BV 30001) (y1 : BV 60004) (y2 : BV 60003) : Prop := - foo x1 x2 = withoutExpectedType! foo y1 y2 + foo x1 x2 = without_expected_type foo y1 y2 @[elabWithoutExpectedType] axiom foo2 {n m : Nat} (a : BV n) (b : BV m) : BV (n - m)