Data.Primitives.Views

Definitions

data Divides : Integer -> Integer -> Type

  View for expressing a number as a multiplication + a remainder

Totality: total
Visibility: public export
Constructors:

DivByZero : Divides x 0

DivBy : (div : Integer) -> (rem : Integer) -> (rem >= 0) && Delay (rem < d) = True -> Divides ((d * div) + rem) d

divides : (val : Integer) -> (d : Integer) -> Divides val d

  Covering function for the `Divides` view

Totality: total
Visibility: public export

data IntegerRec : Integer -> Type

  View for recursion over Integers

Totality: total
Visibility: public export
Constructors:

IntegerZ : IntegerRec 0

IntegerSucc : IntegerRec (-1 + n) -> IntegerRec n

IntegerPred : IntegerRec (1 + negate n) -> IntegerRec (negate n)

integerRec : (x : Integer) -> IntegerRec x

  Covering function for `IntegerRec`

Totality: total
Visibility: public export

data Divides : Int -> Int -> Type

  View for expressing a number as a multiplication + a remainder

Totality: total
Visibility: public export
Constructors:

DivByZero : Divides x 0

DivBy : (div : Int) -> (rem : Int) -> (rem >= 0) && Delay (rem < d) = True -> Divides ((d * div) + rem) d

divides : (val : Int) -> (d : Int) -> Divides val d

  Covering function for the `Divides` view

Totality: total
Visibility: public export

data IntRec : Int -> Type

  View for recursion over Ints

Totality: total
Visibility: public export
Constructors:

IntZ : IntRec 0

IntSucc : IntRec (-1 + n) -> IntRec n

IntPred : IntRec (1 + negate n) -> IntRec (negate n)

intRec : (x : Int) -> IntRec x

  Covering function for `IntRec`

Totality: total
Visibility: public export