@@ -12,9 +12,9 @@ namespace Integer
12 DivByZero : Divides x 0
12 DivByZero : Divides x 0
13 DivBy : (prf : rem >= 0 && rem < d = True) ->
13 DivBy : (prf : rem >= 0 && rem < d = True) ->
14 Divides ((d * div) + rem) d
14 Divides ((d * div) + rem) d
16 ||| Covering function for the `Divides` view
16 ||| Covering function for the `Divides` view
17− export
17+ public export
18 divides : (val : Integer) -> (d : Integer) -> Divides val d
18 divides : (val : Integer) -> (d : Integer) -> Divides val d
19 divides val 0 = DivByZero
19 divides val 0 = DivByZero
20 divides val d
20 divides val d
@@ -22,21 +22,23 @@ namespace Integer
22 let dividend = if d < 0 then -(val `div` abs d)
22 let dividend = if d < 0 then -(val `div` abs d)
23 else val `div` d
23 else val `div` d
24 remainder = abs (val - dividend * d) in
24 remainder = abs (val - dividend * d) in
25− believe_me (DivBy {d} {div = dividend} {rem = remainder}
25+ really_believe_me (DivBy {d} {div = dividend} {rem = remainder}
26− (believe_me (Refl {x = True})))
26+ (really_believe_me (Refl {x = True})))
28 ||| View for recursion over Integers
28 ||| View for recursion over Integers
29 data IntegerRec : Integer -> Type where
30 data IntegerRec : Integer -> Type where
30 IntegerZ : IntegerRec 0
31 IntegerZ : IntegerRec 0
31 IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
32 IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
32 IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)
33 IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)
34 ||| Covering function for `IntegerRec`
35 ||| Covering function for `IntegerRec`
35 integerRec : (x : Integer) -> IntegerRec x
37 integerRec : (x : Integer) -> IntegerRec x
36 integerRec 0 = IntegerZ
38 integerRec 0 = IntegerZ
37 integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
39 integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
38− else believe_me (IntegerPred {n=-x}
40+ else really_believe_me (IntegerPred {n=-x}
39− (assert_total (believe_me (integerRec (x + 1)))))
41+ (assert_total (really_believe_me (integerRec (x + 1)))))
41namespace Int
43namespace Int
42 ||| View for expressing a number as a multiplication + a remainder
44 ||| View for expressing a number as a multiplication + a remainder
@@ -45,13 +47,13 @@ namespace Int
45 DivByZero : Int.Divides x 0
47 DivByZero : Int.Divides x 0
46 DivBy : (prf : rem >= 0 && rem < d = True) ->
48 DivBy : (prf : rem >= 0 && rem < d = True) ->
47 Int.Divides ((d * div) + rem) d
49 Int.Divides ((d * div) + rem) d
49 -- I have assumed, but not actually verified, that this will still
51 -- I have assumed, but not actually verified, that this will still
50 -- give a right result (i.e. still adding up) when the Ints overflow.
52 -- give a right result (i.e. still adding up) when the Ints overflow.
51 -- TODO: Someone please check this and fix if necessary...
53 -- TODO: Someone please check this and fix if necessary...
53 ||| Covering function for the `Divides` view
55 ||| Covering function for the `Divides` view
54− export
56+ public export
55 divides : (val : Int) -> (d : Int) -> Divides val d
57 divides : (val : Int) -> (d : Int) -> Divides val d
56 divides val 0 = DivByZero
58 divides val 0 = DivByZero
57 divides val d
59 divides val d
@@ -59,19 +61,21 @@ namespace Int
59 let dividend = if d < 0 then -(val `div` abs d)
61 let dividend = if d < 0 then -(val `div` abs d)
60 else val `div` d
62 else val `div` d
61 remainder = abs (val - dividend * d) in
63 remainder = abs (val - dividend * d) in
62− believe_me (DivBy {d} {div = dividend} {rem = remainder}
64+ really_believe_me (DivBy {d} {div = dividend} {rem = remainder}
63− (believe_me (Refl {x = True})))
65+ (really_believe_me (Refl {x = True})))
65 ||| View for recursion over Ints
67 ||| View for recursion over Ints
66 data IntRec : Int -> Type where
69 data IntRec : Int -> Type where
67 IntZ : IntRec 0
70 IntZ : IntRec 0
68 IntSucc : IntRec (n - 1) -> IntRec n
71 IntSucc : IntRec (n - 1) -> IntRec n
69 IntPred : IntRec ((-n) + 1) -> IntRec (-n)
72 IntPred : IntRec ((-n) + 1) -> IntRec (-n)
71 ||| Covering function for `IntRec`
74 ||| Covering function for `IntRec`
72 intRec : (x : Int) -> IntRec x
76 intRec : (x : Int) -> IntRec x
73 intRec 0 = IntZ
77 intRec 0 = IntZ
74 intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
78 intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
75− else believe_me (IntPred {n=-x}
79+ else really_believe_me (IntPred {n=-x}
76− (assert_total (believe_me (intRec (x + 1)))))
80+ (assert_total (really_believe_me (intRec (x + 1)))))