Idris2Doc : Data.Primitives.Views

Data.Primitives.Views

Definitions

dataDivides : Integer->Integer->Type
  View for expressing a number as a multiplication + a remainder

Totality: total
Visibility: public export
Constructors:
DivByZero : Dividesx0
DivBy : (div : Integer) -> (rem : Integer) -> (rem>=0) && Delay (rem<d) =True->Divides ((d*div) +rem) d
divides : (val : Integer) -> (d : Integer) ->Dividesvald
  Covering function for the `Divides` view

Totality: total
Visibility: public export
dataIntegerRec : Integer->Type
  View for recursion over Integers

Totality: total
Visibility: public export
Constructors:
IntegerZ : IntegerRec0
IntegerSucc : IntegerRec (-1+n) ->IntegerRecn
IntegerPred : IntegerRec (1+negaten) ->IntegerRec (negaten)
integerRec : (x : Integer) ->IntegerRecx
  Covering function for `IntegerRec`

Totality: total
Visibility: public export
dataDivides : Int->Int->Type
  View for expressing a number as a multiplication + a remainder

Totality: total
Visibility: public export
Constructors:
DivByZero : Dividesx0
DivBy : (div : Int) -> (rem : Int) -> (rem>=0) && Delay (rem<d) =True->Divides ((d*div) +rem) d
divides : (val : Int) -> (d : Int) ->Dividesvald
  Covering function for the `Divides` view

Totality: total
Visibility: public export
dataIntRec : Int->Type
  View for recursion over Ints

Totality: total
Visibility: public export
Constructors:
IntZ : IntRec0
IntSucc : IntRec (-1+n) ->IntRecn
IntPred : IntRec (1+negaten) ->IntRec (negaten)
intRec : (x : Int) ->IntRecx
  Covering function for `IntRec`

Totality: total
Visibility: public export