@@ -133,21 +133,21 @@ instance Ord a => Monoid (MaxiphobicHeap a) where
133133-- Properties
134134--------------------------------------------------------------------------------
135135
136−total absurdBoolDischarge : False = True -> Void
137−absurdBoolDischarge p = replace {P = disjointTy} p ()
138− where
139− total disjointTy : Bool -> Type
140− disjointTy False = ()
141− disjointTy True = Void
136+total
137+absurdBoolDischarge : False = True -> Void
138+absurdBoolDischarge Refl impossible
142139
143−total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
140+total
141+isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
144142isEmptySizeZero Empty p = Refl
145−isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
143+isEmptySizeZero (Node s l e r) Refl impossible
146144
147−total emptyHeapValid : Ord a => isValidHeap (empty {a}) = True
145+total
146+emptyHeapValid : Ord a => isValidHeap (empty {a}) = True
148147emptyHeapValid = Refl
149148
150−total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True
149+total
150+singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True
151151singletonHeapValid e = Refl
152152
153153{-
@@ -161,16 +161,7 @@ mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =
161161 ?mergePreservesValidHeapsBody
162162-}
163163
164−--------------------------------------------------------------------------------
165−-- Proofs
166−--------------------------------------------------------------------------------
167164
168−isEmptySizeZeroNodeAbsurd = proof {
169− intros;
170− refine void;
171− refine absurdBoolDischarge;
172− exact p;
173−}
174165
175166--------------------------------------------------------------------------------
176167-- Debug