From 6d10b7594f487bdfbef99d05bda34405dd85c8b8 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 16 Nov 2025 14:24:46 +0100
Subject: Lean 4.23

---
 Common/List.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Common/List.lean')

diff --git a/Common/List.lean b/Common/List.lean
index f6c0de5..9db3b86 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -23,7 +23,7 @@ def quicksortBy {α : Type} (pred : α → α → Bool): List α → List α
   termination_by l => l.length
   decreasing_by
     all_goals
-      simp +arith only [unattach_filter, unattach_attach, length_cons, gt_iff_lt, listFilterSmallerOrEqualList]
+      simp +arith only [unattach_filter, unattach_attach, length_cons, listFilterSmallerOrEqualList]
 
 def quicksort {α : Type} [Ord α] : List α → List α := quicksortBy λ a b ↦ Ord.compare a b == Ordering.lt
 
-- 
cgit v1.2.3