From 42f1e16f4448a9eef8b835c35d79ec4449b13a06 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Aug 2021 06:59:46 -0700 Subject: [PATCH] chore: fix `calc` test --- tests/lean/run/calc.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/calc.lean b/tests/lean/run/calc.lean index e5ce0cbbbe..c4fa26ceda 100644 --- a/tests/lean/run/calc.lean +++ b/tests/lean/run/calc.lean @@ -4,7 +4,7 @@ variable (pf12 : t1 = t2) (pf23 : t2 = t3) (pf34 : t3 = t4) theorem foo : t1 = t4 := calc t1 = t2 := pf12 - _ = t3 := id + _ = t3 := pf23 _ = t4 := pf34 variable (t5 : Nat)