Idris2Doc : Prelude.Num

Prelude.Num

(*) : Numty => ty -> ty -> ty
Totality: total
Fixity Declaration: infixl operator, level 9
(+) : Numty => ty -> ty -> ty
Totality: total
Fixity Declaration: infixl operator, level 8
negate : Negty => ty -> ty
The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

Totality: total
Fixity Declaration: prefix operator, level 10
(-) : Negty => ty -> ty -> ty
Totality: total
Fixity Declarations:
infixl operator, level 8
prefix operator, level 10
(/) : Fractionalty => ty -> ty -> ty
Totality: total
Fixity Declaration: infixl operator, level 9
interfaceAbs : Type -> Type
Numbers for which the absolute value is defined should implement `Abs`.

Parameters: ty
Constraints: Num ty
Constructor: MkAbs
Methods:
abs : ty -> ty
Absolute value.

Implementations:
AbsInteger
AbsInt
AbsInt8
AbsInt16
AbsInt32
AbsInt64
AbsBits8
AbsBits16
AbsBits32
AbsBits64
AbsDouble
interfaceFractional : Type -> Type
Parameters: ty
Constraints: Num ty
Constructor: MkFractional
Methods:
(/) : ty -> ty -> ty
Fixity Declaration: infixl operator, level 9
recip : ty -> ty

Implementation:
FractionalDouble
interfaceIntegral : Type -> Type
Parameters: ty
Constraints: Num ty
Constructor: MkIntegral
Methods:
div : ty -> ty -> ty
Fixity Declaration: infixl operator, level 9
mod : ty -> ty -> ty
Fixity Declaration: infixl operator, level 9

Implementations:
IntegralInteger
IntegralInt
IntegralInt8
IntegralInt16
IntegralInt32
IntegralInt64
IntegralBits8
IntegralBits16
IntegralBits32
IntegralBits64
interfaceNeg : Type -> Type
The `Neg` interface defines operations on numbers which can be negative.

Parameters: ty
Constraints: Num ty
Constructor: MkNeg
Methods:
negate : ty -> ty
The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

Fixity Declaration: prefix operator, level 10
(-) : ty -> ty -> ty
Fixity Declarations:
infixl operator, level 8
prefix operator, level 10

Implementations:
NegInteger
NegInt
NegInt8
NegInt16
NegInt32
NegInt64
NegBits8
NegBits16
NegBits32
NegBits64
NegDouble
interfaceNum : Type -> Type
The Num interface defines basic numerical arithmetic.

Parameters: ty
Constructor: MkNum
Methods:
(+) : ty -> ty -> ty
Fixity Declaration: infixl operator, level 8
(*) : ty -> ty -> ty
Fixity Declaration: infixl operator, level 9
fromInteger : Integer -> ty
Conversion from Integer.

Implementations:
NumInteger
NumInt
NumInt8
NumInt16
NumInt32
NumInt64
NumBits8
NumBits16
NumBits32
NumBits64
NumDouble
NumNat
abs : Absty => ty -> ty
Absolute value.

Totality: total
defaultInteger : NumInteger
Totality: total
div : Integralty => ty -> ty -> ty
Totality: total
Fixity Declaration: infixl operator, level 9
fromInteger : Numty => Integer -> ty
Conversion from Integer.

Totality: total
mod : Integralty => ty -> ty -> ty
Totality: total
Fixity Declaration: infixl operator, level 9
negate : Negty => ty -> ty
The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

Totality: total
Fixity Declaration: prefix operator, level 10
recip : Fractionalty => ty -> ty
Totality: total