@@ -2,6 +2,7 @@
22module Data.Nat
33
44import Data.Fin
5+import Data.So
56
67import Control.WellFounded
78
@@ -41,7 +42,7 @@ lteToLt' {n = S k} (LTESucc x) = ltSuccSucc $ lteToLt' x
4142||| Convert from LT' to LTE
4243ltToLTE : LT' n m -> LTE (S n) m
4344ltToLTE LTSucc = lteRefl
44−ltToLTE (LTStep lt) = lteSucc $ ltToLTE lt
45+ltToLTE (LTStep lt) = lteSuccRight $ ltToLTE lt
4546
4647||| Subtraction gives a result that is actually smaller.
4748minusLT' : (x,y : Nat) -> x - y `LT'` S x
@@ -95,14 +96,6 @@ toFinAndBack : (x : Nat) -> (diff : Nat) -> finToNat (toFin x diff) = x
9596toFinAndBack Z diff = Refl
9697toFinAndBack (S k) diff = cong (toFinAndBack k diff)
9798
98−||| This property is not the case.
99−|||
100−||| Use this to ensure properties in implicit arguments.
101−|||
102−||| @ p the property that doesn't hold
103−Nope : Dec p -> Type
104−Nope (Yes _) = Void
105−Nope (No _) = ()
10699
107100||| The accessibilty predicate used for division.
108101private
@@ -123,7 +116,7 @@ accPlusLT' {j = S j} {k = k} = rewrite sym $ plusSuccRightSucc k (S j) in
123116||| @ nonzero division by zero is nonsense
124117total -- yay!
125118divMod : (dividend, divisor : Nat) ->
126− {auto nonzero : Nope (decEq divisor Z)} ->
119+ {auto nonzero : So (not (decAsBool (decEq divisor Z)))} ->
127120 DivMod dividend divisor
128121divMod _ Z {nonzero} = absurd nonzero
129122divMod Z (S k) = DivModRes 0 FZ Refl
@@ -136,7 +129,7 @@ divMod (S j) (S k) {nonzero} = wfInd {P=P} stepDiv (S j) (S k) nonzero
136129 |||
137130 ||| @ dividend the dividend to recurse over
138131 P : (dividend : Nat) -> Type
139− P dividend = (divisor : Nat) -> (nonzero : Nope (decEq divisor Z)) -> DivMod dividend divisor
132+ P dividend = (divisor : Nat) -> (nonzero : So (not (decAsBool (decEq divisor Z)))) -> DivMod dividend divisor
140133
141134
142135 ||| Well-founded recursion needs a recursion operator.
@@ -160,7 +153,7 @@ divMod (S j) (S k) {nonzero} = wfInd {P=P} stepDiv (S j) (S k) nonzero
160153 in sym $ cong (plusZeroRightNeutral j)
161154 -- if n > m, then n = m + d, and the quotient is 1 + ((n - m) / m) with the same remainder
162155 stepDiv (S (plus k (S diff))) rec (S k) nonzero | CmpGT diff =
163− let res = rec (S diff) accPlusLT' (S k) ()
156+ let res = rec (S diff) accPlusLT' (S k) Oh
164157 in case res of
165158 DivModRes quotient remainder ok =>
166159 DivModRes (S quotient) remainder $