git.iko.soy/Idris-dev
on master help sign in
Fix proof script deprecation warnings
6cf7f5aDavid Raymond Christiansen
libs/contrib/Data/Heap.idr+10−19
compare with master
unifiedsplit
@@ -133,21 +133,21 @@ instance Ord a => Monoid (MaxiphobicHeap a) where
133-- Properties
133-- Properties
134--------------------------------------------------------------------------------
134--------------------------------------------------------------------------------
135
135
136+total
136−total absurdBoolDischarge : False = True -> Void
137+absurdBoolDischarge : False = True -> Void
137−absurdBoolDischarge p = replace {P = disjointTy} p ()
138+absurdBoolDischarge Refl impossible
138− where
139− total disjointTy : Bool -> Type
140− disjointTy False = ()
141− disjointTy True = Void
142
139
140+total
143−total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
141+isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
144isEmptySizeZero Empty p = Refl
142isEmptySizeZero Empty p = Refl
145−isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
143+isEmptySizeZero (Node s l e r) Refl impossible
146
144
145+total
147−total emptyHeapValid : Ord a => isValidHeap (empty {a}) = True
146+emptyHeapValid : Ord a => isValidHeap (empty {a}) = True
148emptyHeapValid = Refl
147emptyHeapValid = Refl
149
148
149+total
150−total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True
150+singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True
151singletonHeapValid e = Refl
151singletonHeapValid e = Refl
152
152
153{-
153{-
@@ -161,16 +161,7 @@ mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =
161 ?mergePreservesValidHeapsBody
161 ?mergePreservesValidHeapsBody
162-}
162-}
163
163
164−--------------------------------------------------------------------------------
165−-- Proofs
166−--------------------------------------------------------------------------------
167
164
168−isEmptySizeZeroNodeAbsurd = proof {
169− intros;
170− refine void;
171− refine absurdBoolDischarge;
172− exact p;
173−}
174
165
175--------------------------------------------------------------------------------
166--------------------------------------------------------------------------------
176-- Debug
167-- Debug