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

---
 Common/Parsing.lean | 1 -
 1 file changed, 1 deletion(-)

(limited to 'Common')

diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index 348db25..637f807 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -103,7 +103,6 @@ protected def RectangularGrid.parseSingleLine (parseCharacter : Char → Except
       RectangularGrid.parseSingleLine parseCharacter (alreadyParsed.push element) (remainingLine.drop 1)
 termination_by remainingLine.bsize
 decreasing_by
-  simp_wf
   simp only [Substring.isEmpty, Substring.bsize, Nat.sub_eq, beq_iff_eq] at _h₁
   simp only [Substring.drop, Substring.bsize, Substring.nextn, Substring.next, String.Pos.add_byteIdx, Nat.sub_eq]
   split
-- 
cgit v1.2.3