IdrisDoc: Prelude.Interfaces

Prelude.Interfaces

thenCompare : Ordering -> Lazy Ordering -> Ordering

Compose two comparisons into the lexicographic product

modInt : Int -> Int -> Int
modBigInt : Integer -> Integer -> Integer
modB8 : Bits8 -> Bits8 -> Bits8
modB64 : Bits64 -> Bits64 -> Bits64
modB32 : Bits32 -> Bits32 -> Bits32
modB16 : Bits16 -> Bits16 -> Bits16
intToBool : Int -> Bool
divInt : Int -> Int -> Int
divBigInt : Integer -> Integer -> Integer
divB8 : Bits8 -> Bits8 -> Bits8
divB64 : Bits64 -> Bits64 -> Bits64
divB32 : Bits32 -> Bits32 -> Bits32
divB16 : Bits16 -> Bits16 -> Bits16
default#recip : Fractional ty => ty -> ty
default#min : Ord ty => ty -> ty -> ty
default#max : Ord ty => ty -> ty -> ty
default#>= : Ord ty => ty -> ty -> Bool
default#> : Ord ty => ty -> ty -> Bool
default#== : Eq ty => ty -> ty -> Bool
default#<= : Ord ty => ty -> ty -> Bool
default#< : Ord ty => ty -> ty -> Bool
default#/= : Eq ty => ty -> ty -> Bool
boolOp : (a -> a -> Int) -> a -> a -> Bool
data Ordering : Type
LT : Ordering
EQ : Ordering
GT : Ordering
interface Ord 

The Ord interface defines comparison operations on ordered data types.

compare : Ord ty => ty -> ty -> Ordering
(<) : Ord ty => ty -> ty -> Bool
Fixity
Left associative, precedence 6
(>) : Ord ty => ty -> ty -> Bool
Fixity
Left associative, precedence 6
(<=) : Ord ty => ty -> ty -> Bool
Fixity
Left associative, precedence 6
(>=) : Ord ty => ty -> ty -> Bool
Fixity
Left associative, precedence 6
max : Ord ty => ty -> ty -> ty
min : Ord ty => ty -> ty -> ty
interface Num 

The Num interface defines basic numerical arithmetic.

(+) : Num ty => ty -> ty -> ty
Fixity
Left associative, precedence 8
(*) : Num ty => ty -> ty -> ty
Fixity
Left associative, precedence 9
fromInteger : Num ty => Integer -> ty

Conversion from Integer.

interface Neg 

The Neg interface defines operations on numbers which can be negative.

negate : Neg ty => ty -> ty

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

(-) : Neg ty => ty -> ty -> ty
Fixity
Left associative, precedence 8
abs : Neg ty => ty -> ty

Absolute value

interface MinBound 
minBound : MinBound b => b

The lower bound for the type

interface MaxBound 
maxBound : MaxBound b => b

The upper bound for the type

interface Integral 
div : Integral ty => ty -> ty -> ty
mod : Integral ty => ty -> ty -> ty
interface Fractional 
(/) : Fractional ty => ty -> ty -> ty
Fixity
Left associative, precedence 9
recip : Fractional ty => ty -> ty
interface Eq 

The Eq interface defines inequality and equality.

(==) : Eq ty => ty -> ty -> Bool
Fixity
Left associative, precedence 5
(/=) : Eq ty => ty -> ty -> Bool
Fixity
Left associative, precedence 5