@@ -24,6 +24,19 @@ namespace Integer
2424 believe_me (DivBy {d} {div = dividend} {rem = remainder}
2525 (believe_me (Refl {x = True})))
2626
27+ ||| View for recursion over Integers
28+ data IntegerRec : Integer -> Type where
29+ IntegerZ : IntegerRec 0
30+ IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
31+ IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)
32+
33+ ||| Covering function for `IntegerRec`
34+ integerRec : (x : Integer) -> IntegerRec x
35+ integerRec 0 = IntegerZ
36+ integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
37+ else believe_me (IntegerPred {n=-x}
38+ (assert_total (believe_me (integerRec (x + 1)))))
39+
2740namespace Int
2841 ||| View for expressing a number as a multiplication + a remainder
2942 public export
@@ -47,3 +60,16 @@ namespace Int
4760 believe_me (DivBy {d} {div = dividend} {rem = remainder}
4861 (believe_me (Refl {x = True})))
4962
63+ ||| View for recursion over Ints
64+ data IntRec : Int -> Type where
65+ IntZ : IntRec 0
66+ IntSucc : IntRec (n - 1) -> IntRec n
67+ IntPred : IntRec ((-n) + 1) -> IntRec (-n)
68+
69+ ||| Covering function for `IntRec`
70+ intRec : (x : Int) -> IntRec x
71+ intRec 0 = IntZ
72+ intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
73+ else believe_me (IntPred {n=-x}
74+ (assert_total (believe_me (intRec (x + 1)))))
75+