@@ -12,7 +12,7 @@ namespace Integer
1212 DivByZero : Divides x 0
1313 DivBy : (prf : rem >= 0 && rem < d = True) ->
1414 Divides ((d * div) + rem) d
15−
15+
1616 ||| Covering function for the `Divides` view
1717 public export
1818 divides : (val : Integer) -> (d : Integer) -> Divides val d
@@ -22,21 +22,23 @@ namespace Integer
2222 let dividend = if d < 0 then -(val `div` abs d)
2323 else val `div` d
2424 remainder = abs (val - dividend * d) in
25− believe_me (DivBy {d} {div = dividend} {rem = remainder}
26− (believe_me (Refl {x = True})))
25+ really_believe_me (DivBy {d} {div = dividend} {rem = remainder}
26+ (really_believe_me (Refl {x = True})))
2727
2828 ||| View for recursion over Integers
29+ public export
2930 data IntegerRec : Integer -> Type where
3031 IntegerZ : IntegerRec 0
3132 IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
3233 IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)
33−
34+
3435 ||| Covering function for `IntegerRec`
36+ public export
3537 integerRec : (x : Integer) -> IntegerRec x
3638 integerRec 0 = IntegerZ
3739 integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
38− else believe_me (IntegerPred {n=-x}
39− (assert_total (believe_me (integerRec (x + 1)))))
40+ else really_believe_me (IntegerPred {n=-x}
41+ (assert_total (really_believe_me (integerRec (x + 1)))))
4042
4143namespace Int
4244 ||| View for expressing a number as a multiplication + a remainder
@@ -45,7 +47,7 @@ namespace Int
4547 DivByZero : Int.Divides x 0
4648 DivBy : (prf : rem >= 0 && rem < d = True) ->
4749 Int.Divides ((d * div) + rem) d
48−
50+
4951 -- I have assumed, but not actually verified, that this will still
5052 -- give a right result (i.e. still adding up) when the Ints overflow.
5153 -- TODO: Someone please check this and fix if necessary...
@@ -59,19 +61,21 @@ namespace Int
5961 let dividend = if d < 0 then -(val `div` abs d)
6062 else val `div` d
6163 remainder = abs (val - dividend * d) in
62− believe_me (DivBy {d} {div = dividend} {rem = remainder}
63− (believe_me (Refl {x = True})))
64+ really_believe_me (DivBy {d} {div = dividend} {rem = remainder}
65+ (really_believe_me (Refl {x = True})))
6466
6567 ||| View for recursion over Ints
68+ public export
6669 data IntRec : Int -> Type where
6770 IntZ : IntRec 0
6871 IntSucc : IntRec (n - 1) -> IntRec n
6972 IntPred : IntRec ((-n) + 1) -> IntRec (-n)
70−
73+
7174 ||| Covering function for `IntRec`
75+ public export
7276 intRec : (x : Int) -> IntRec x
7377 intRec 0 = IntZ
7478 intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
75− else believe_me (IntPred {n=-x}
76− (assert_total (believe_me (intRec (x + 1)))))
77−
79+ else really_believe_me (IntPred {n=-x}
80+ (assert_total (really_believe_me (intRec (x + 1)))))
81+