Prelude.Num

Definitions

interface Num : 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:

Num Integer

Num Int

Num Int8

Num Int16

Num Int32

Num Int64

Num Bits8

Num Bits16

Num Bits32

Num Bits64

Num Double

Num Nat

(+) : Num ty => ty -> ty -> ty

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

(*) : Num ty => ty -> ty -> ty

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

fromInteger : Num ty => Integer -> ty

  Conversion from Integer.

Totality: total
Visibility: public export

interface Neg : 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:

Neg Integer

Neg Int

Neg Int8

Neg Int16

Neg Int32

Neg Int64

Neg Bits8

Neg Bits16

Neg Bits32

Neg Bits64

Neg Double

negate : Neg ty => 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 : Neg ty => ty -> ty

  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 10

(-) : Neg ty => ty -> ty -> ty

Totality: total
Visibility: public export
Fixity Declarations:
infixl operator, level 8
prefix operator, level 10

subtract : Neg ty => 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

interface Abs : 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:

Abs Integer

Abs Int

Abs Int8

Abs Int16

Abs Int32

Abs Int64

Abs Bits8

Abs Bits16

Abs Bits32

Abs Bits64

Abs Double

abs : Abs ty => ty -> ty

  Absolute value.

Totality: total
Visibility: public export

interface Fractional : Type -> Type

Parameters: ty
Constraints: Num ty
Constructor: 

MkFractional

Methods:

(/) : ty -> ty -> ty

Fixity Declaration: infixl operator, level 9

recip : ty -> ty

Implementation: 

Fractional Double

(/) : Fractional ty => ty -> ty -> ty

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

recip : Fractional ty => ty -> ty

Totality: total
Visibility: public export

interface Integral : 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:

Integral Integer

Integral Int

Integral Int8

Integral Int16

Integral Int32

Integral Int64

Integral Bits8

Integral Bits16

Integral Bits32

Integral Bits64

div : Integral ty => ty -> ty -> ty

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

mod : Integral ty => ty -> ty -> ty

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

defaultInteger : Num Integer

Totality: total
Visibility: public export