Idris2Doc : Prelude.Num

Prelude.Num

Definitions

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:
NumNat
NumInteger
NumInt
NumInt8
NumInt16
NumInt32
NumInt64
NumBits8
NumBits16
NumBits32
NumBits64
NumDouble
(+) : Numty=>ty->ty->ty
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8
(*) : Numty=>ty->ty->ty
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9
fromInteger : Numty=>Integer->ty
  Conversion from Integer.

Totality: total
Visibility: public export
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
negate : Negty=>ty->ty
  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 10
negate : Negty=>ty->ty
  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 10
(-) : Negty=>ty->ty->ty
Totality: total
Visibility: public export
Fixity Declarations:
infixl operator, level 8
prefix operator, level 10
subtract : Negty=>ty->ty->ty
  A convenience alias for `(-)`, this function enables partial application of subtraction on the
right-hand operand as
```idris example
(`subtract` 1)
```
This contrasts with `(- 1)`, which is parsed as `-1`.

Totality: total
Visibility: export
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
abs : Absty=>ty->ty
  Absolute value.

Totality: total
Visibility: public export
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
(/) : Fractionalty=>ty->ty->ty
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9
recip : Fractionalty=>ty->ty
Totality: total
Visibility: public export
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
div : Integralty=>ty->ty->ty
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9
mod : Integralty=>ty->ty->ty
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9
defaultInteger : NumInteger
Totality: total
Visibility: public export