@@ -5,6 +5,7 @@
55
66module Data.Heap
77
8+%default total
89%access public
910
1011abstract data MaxiphobicHeap : Type -> Type where
@@ -82,12 +83,12 @@ insert e = merge $ singleton e
8283--------------------------------------------------------------------------------
8384
8485findMinimum : (h : MaxiphobicHeap a) -> (isEmpty h = False) -> a
85−findMinimum Empty p = ?findMinimumEmptyAbsurd
86−findMinimum (Node s l e r) p = e
86+findMinimum Empty refl impossible
87+findMinimum (Node s l e r) p = e
8788
8889deleteMinimum : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> MaxiphobicHeap a
89−deleteMinimum Empty p = ?deleteMinimumEmptyAbsurd
90−deleteMinimum (Node s l e r) p = merge l r
90+deleteMinimum Empty refl impossible
91+deleteMinimum (Node s l e r) p = merge l r
9192
9293--------------------------------------------------------------------------------
9394-- Conversions to and from lists (and a derived heap sorting algorithm)
@@ -173,22 +174,6 @@ isEmptySizeZeroNodeAbsurd = proof {
173174 exact p;
174175}
175176
176−findMinimumEmptyAbsurd = proof {
177− intros;
178− refine FalseElim;
179− refine absurdBoolDischarge;
180− rewrite p;
181− trivial;
182−}
183−
184−deleteMinimumEmptyAbsurd = proof {
185− intros;
186− refine FalseElim;
187− refine absurdBoolDischarge;
188− rewrite p;
189− trivial;
190−}
191−
192177--------------------------------------------------------------------------------
193178-- Debug
194179--------------------------------------------------------------------------------