Idris2Doc : Data.INTEGER

Data.INTEGER(source)

Definitions

dataINTEGER : Type
Totality: total
Visibility: public export
Constructors:
Z : INTEGER
PS : Nat->INTEGER
NS : Nat->INTEGER

Hints:
CastNatINTEGER
CastIntegerINTEGER
CastINTEGERInteger
NegINTEGER
NumINTEGER
ShowINTEGER
add : INTEGER->INTEGER->INTEGER
Totality: total
Visibility: public export
mult : INTEGER->INTEGER->INTEGER
Totality: total
Visibility: public export
plusZeroRightNeutral : (m : INTEGER) ->m+Z=m
Totality: total
Visibility: export
plusCommutative : (m : INTEGER) -> (n : INTEGER) ->m+n=n+m
Totality: total
Visibility: export
castPlus : (m : Nat) -> (n : Nat) ->theINTEGER (cast (m+n)) =castm+castn
Totality: total
Visibility: export
unfoldPS : (m : Nat) ->PSm=1+castm
Totality: total
Visibility: export
unfoldNS : (m : Nat) ->NSm=-1-castm
Totality: total
Visibility: export
difference : Nat->Nat->INTEGER
Totality: total
Visibility: export
differenceZeroRight : (n : Nat) ->differencen0=castn
Totality: total
Visibility: export
minusSuccSucc : (m : Nat) -> (n : Nat) ->theINTEGER (cast (Sm) -cast (Sn)) =castm-castn
Totality: total
Visibility: export
unfoldDifference : (m : Nat) -> (n : Nat) ->differencemn=castm-castn
Totality: total
Visibility: export
negateInvolutive : (m : INTEGER) ->negate (negatem) =m
Totality: total
Visibility: export
negatePlus : (m : INTEGER) -> (n : INTEGER) ->negate (m+n) =negatem+negaten
Totality: total
Visibility: export
negateDifference : (m : Nat) -> (n : Nat) ->negate (differencemn) =differencenm
Totality: total
Visibility: export
minusZeroRight : (m : INTEGER) ->m-Z=m
Totality: total
Visibility: export
plusInverse : (m : INTEGER) ->m-m=Z
Totality: total
Visibility: export
plusAssociative : (m : INTEGER) -> (n : INTEGER) -> (p : INTEGER) ->m+ (n+p) = (m+n) +p
Totality: total
Visibility: export