@@ -2,6 +2,7 @@
2module Data.Nat
2module Data.Nat
4import Data.Fin
4import Data.Fin
6import Control.WellFounded
7import Control.WellFounded
@@ -41,7 +42,7 @@ lteToLt' {n = S k} (LTESucc x) = ltSuccSucc $ lteToLt' x
41||| Convert from LT' to LTE
42||| Convert from LT' to LTE
42ltToLTE : LT' n m -> LTE (S n) m
43ltToLTE : LT' n m -> LTE (S n) m
43ltToLTE LTSucc = lteRefl
44ltToLTE LTSucc = lteRefl
44−ltToLTE (LTStep lt) = lteSucc $ ltToLTE lt
45+ltToLTE (LTStep lt) = lteSuccRight $ ltToLTE lt
46||| Subtraction gives a result that is actually smaller.
47||| Subtraction gives a result that is actually smaller.
47minusLT' : (x,y : Nat) -> x - y `LT'` S x
48minusLT' : (x,y : Nat) -> x - y `LT'` S x
@@ -95,14 +96,6 @@ toFinAndBack : (x : Nat) -> (diff : Nat) -> finToNat (toFin x diff) = x
95toFinAndBack Z diff = Refl
96toFinAndBack Z diff = Refl
96toFinAndBack (S k) diff = cong (toFinAndBack k diff)
97toFinAndBack (S k) diff = cong (toFinAndBack k diff)
98−||| This property is not the case.
100−||| Use this to ensure properties in implicit arguments.
102−||| @ p the property that doesn't hold
107||| The accessibilty predicate used for division.
100||| The accessibilty predicate used for division.
@@ -123,7 +116,7 @@ accPlusLT' {j = S j} {k = k} = rewrite sym $ plusSuccRightSucc k (S j) in
123||| @ nonzero division by zero is nonsense
116||| @ nonzero division by zero is nonsense
124total -- yay!
117total -- yay!
125divMod : (dividend, divisor : Nat) ->
118divMod : (dividend, divisor : Nat) ->
126− {auto nonzero : Nope (decEq divisor Z)} ->
119+ {auto nonzero : So (not (decAsBool (decEq divisor Z)))} ->
127 DivMod dividend divisor
120 DivMod dividend divisor
128divMod _ Z {nonzero} = absurd nonzero
121divMod _ Z {nonzero} = absurd nonzero
129divMod Z (S k) = DivModRes 0 FZ Refl
122divMod 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
137 ||| @ dividend the dividend to recurse over
130 ||| @ dividend the dividend to recurse over
138 P : (dividend : Nat) -> Type
131 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
142 ||| Well-founded recursion needs a recursion operator.
135 ||| 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
160 in sym $ cong (plusZeroRightNeutral j)
153 in sym $ cong (plusZeroRightNeutral j)
161 -- if n > m, then n = m + d, and the quotient is 1 + ((n - m) / m) with the same remainder
154 -- if n > m, then n = m + d, and the quotient is 1 + ((n - m) / m) with the same remainder
162 stepDiv (S (plus k (S diff))) rec (S k) nonzero | CmpGT diff =
155 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
164 in case res of
157 in case res of
165 DivModRes quotient remainder ok =>
158 DivModRes quotient remainder ok =>
166 DivModRes (S quotient) remainder $
159 DivModRes (S quotient) remainder $