From 4f4c8f45cd5ed150da2d6c43bb5c030813567e31 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Dec 2020 16:27:38 -0800 Subject: [PATCH] chore: fix tests --- tests/lean/run/alg.lean | 2 +- tests/lean/scopedunifhint.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/run/alg.lean b/tests/lean/run/alg.lean index a3339260a9..903866a6a4 100644 --- a/tests/lean/run/alg.lean +++ b/tests/lean/run/alg.lean @@ -73,4 +73,4 @@ theorem mul_inv_rev [Group α] (a b : α) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by rw [mul_assoc, ← mul_assoc b, mul_right_inv, one_mul, mul_right_inv] theorem mul_inv [CommGroup α] (a b : α) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by - rw [mul_inv_rev, mul_comm]; rfl + rw [mul_inv_rev, mul_comm] diff --git a/tests/lean/scopedunifhint.lean b/tests/lean/scopedunifhint.lean index 9837d870df..4ab8507522 100644 --- a/tests/lean/scopedunifhint.lean +++ b/tests/lean/scopedunifhint.lean @@ -40,7 +40,7 @@ open Algebra -- activate unification hints section Sec1 -set_option trace.Meta.debug true +-- set_option trace.Meta.debug true -- This hint is only active in this section local unif_hint (s : Magma) (m : Magma) (n : Magma) (β : Type u) (δ : Type v) where m.α =?= β