max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-28 10:55:48 -07:00
parent 8d9626dab7
commit 10d43492ba
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/heapSort.lean.expected.out
View file

@ -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)