From 10d43492ba17f80c3fb4ea19aeb4d7e7bc368e47 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 28 Apr 2022 10:55:48 -0700 Subject: [PATCH] chore: fix test --- tests/lean/heapSort.lean.expected.out | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/lean/heapSort.lean.expected.out b/tests/lean/heapSort.lean.expected.out index ab411359bb..30763ff7e8 100644 --- a/tests/lean/heapSort.lean.expected.out +++ b/tests/lean/heapSort.lean.expected.out @@ -4,8 +4,8 @@ heapSort.lean:61:30-61:35: warning: declaration uses 'sorry' heapSort.lean:110:29-110:34: warning: declaration uses 'sorry' @Array.heapSort.loop._eq_1 : ∀ {α : Type u_1} (lt : α → α → Bool) (a : BinaryHeap α fun y x => lt x y) (out : Array α), Array.heapSort.loop lt a out = - match BinaryHeap.max a, (_ : BinaryHeap.max a = BinaryHeap.max a) with - | none, e => out - | some x, e => + match e : BinaryHeap.max a with + | none => out + | some x => let_fun this := (_ : BinaryHeap.size (BinaryHeap.popMax a) < BinaryHeap.size a); Array.heapSort.loop lt (BinaryHeap.popMax a) (Array.push out x)