From bb6cbe0fe0c415fee1ece7980b0667055b0ed2db Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Tue, 17 Dec 2024 20:00:48 +0100
Subject: Remove useless simp_wf tactic calls

---
 Day12.lean | 1 -
 1 file changed, 1 deletion(-)

(limited to 'Day12.lean')

diff --git a/Day12.lean b/Day12.lean
index a9aa172..63410be 100644
--- a/Day12.lean
+++ b/Day12.lean
@@ -72,7 +72,6 @@ where
       | .ok v => parseLeftBlock (s.drop 1) $ v :: p
   termination_by s => s.bsize
   decreasing_by
-    simp_wf
     rename_i h₁
     apply Substring.drop_bsize_dec _ _ h₁ Nat.one_ne_zero
   parseMaskChar : Char → Except ParsingError SpringState := λ
-- 
cgit v1.2.3