From 6a7830cb717a23c7a5ea5d43a59dbb2886b35991 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 24 Jan 2025 19:24:54 -0800 Subject: [PATCH] fix: Remove spurious print --- Test/Proofs.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index e13e528..bf43bf6 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -750,8 +750,6 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do addTest $ assertUnreachable $ other.toString return () - let iex : InternalExceptionId := { idx := 4 } - IO.println s!"{← iex.getName}" let tactic := "simpa [h] using And.imp_left h _" --let state2 ← match ← state1.tacticOn 0 tactic with -- | .success state => pure state