From 6ed99b77e986560b09e49c9dec4ceff2cd196f5f Mon Sep 17 00:00:00 2001
From: Jannis Limperg <jannis@limperg.de>
Date: Fri, 13 Aug 2021 13:08:49 +0200
Subject: [PATCH] chore: rm redundant branch in BinomialHeap.toList

---
 src/Std/Data/BinomialHeap.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Std/Data/BinomialHeap.lean b/src/Std/Data/BinomialHeap.lean
index 643b3c29bb..b1ee7d4e93 100644
--- a/src/Std/Data/BinomialHeap.lean
+++ b/src/Std/Data/BinomialHeap.lean
@@ -87,11 +87,10 @@ def tail (lt : α → α → Bool) : Heap α → Heap α
     let rest          := hhs.eraseIdx minIdx
     min.children.foldl (merge lt) (heap rest)
 
-partial def toList (lt : α → α → Bool) : Heap α → List α
-  | Heap.empty => []
-  | h          => match head? lt h with
-    | none   => []
-    | some a => a :: toList lt (tail lt h)
+partial def toList (lt : α → α → Bool) (h : Heap α) : List α :=
+  match head? lt h with
+  | none   => []
+  | some a => a :: toList lt (tail lt h)
 
 inductive WellFormed (lt : α → α → Bool) : Heap α → Prop where
   | emptyWff                  : WellFormed lt empty