Overloaded Operations

Equality

Eq
  (==)        : {a}    (Eq a) => a -> a -> Bit
  (!=)        : {a}    (Eq a) => a -> a -> Bit
  (===)       : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
  (!==)       : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)

Instances
Type	Condition
`Bit`
`Integer`
`Rational`
`Z n`	`fin n`, `n >= 1`
`Float e p`	`ValidFloat e p`
`[n] a`	`fin n`, `Eq a`
`(a,b)`	`Eq a`, `Eq b`

Comparisons

Cmp
  (<)         : {a} (Cmp a) => a -> a -> Bit
  (>)         : {a} (Cmp a) => a -> a -> Bit
  (<=)        : {a} (Cmp a) => a -> a -> Bit
  (>=)        : {a} (Cmp a) => a -> a -> Bit
  min         : {a} (Cmp a) => a -> a -> a
  max         : {a} (Cmp a) => a -> a -> a
  abs         : {a} (Cmp a, Ring a) => a -> a

Instances
Type	Condition
`Bit`
`Integer`
`Rational`
`Float e p`	`ValidFloat e p`
`[n] a`	`fin n`, `Cmp a`
`(a,b)`	`Cmp a`, `Cmp b`

Signed Comparisons

SignedCmp
  (<$)        : {a} (SignedCmp a) => a -> a -> Bit
  (>$)        : {a} (SignedCmp a) => a -> a -> Bit
  (<=$)       : {a} (SignedCmp a) => a -> a -> Bit
  (>=$)       : {a} (SignedCmp a) => a -> a -> Bit

Instances
Type	Condition
`[n] Bit`	`fin n`, `n >= 1`
`[n] a`	`fin n`, `SignedCmp a`, `a /= Bit`
`(a,b)`	`SignedCmp a`, `SignedCmp b`

Zero

Zero
  zero        : {a} (Zero a) => a

Instances
Type	Condition
`Bit`
`Integer`
`Rational`
`Z n`	`fin n`, `n >= 1`
`Float e p`	`ValidFloat e p`
`[n] a`	`Zero a`
`a -> b`	`Zero b`
`(a,b)`	`Zero a`, `Zero b`

Logical Operations

Logic
  (&&)        : {a} (Logic a) => a -> a -> a
  (||)        : {a} (Logic a) => a -> a -> a
  (^)         : {a} (Logic a) => a -> a -> a
  complement  : {a} (Logic a) => a -> a

Instances
Type	Condition
`Bit`
`[n] a`	`Logic a`
`a -> b`	`Logic b`
`(a,b)`	`Logic a`, `Logic b`

Basic Arithmetic

Ring
  fromInteger : {a} (Ring a) => Integer -> a
  (+)         : {a} (Ring a) => a -> a -> a
  (-)         : {a} (Ring a) => a -> a -> a
  (*)         : {a} (Ring a) => a -> a -> a
  negate      : {a} (Ring a) => a -> a
  (^^)        : {a, e} (Ring a, Integral e) => a -> e -> a

Instances
Type	Condition
`Integer`
`Rational`
`Z n`	`fin n`, `n >= 1`
`Float e p`	`ValidFloat e p`
`[n] Bit`	`fin n`
`[n] a`	`Ring a`, `a /= Bit`
`a -> b`	`Ring b`
`(a,b)`	`Ring a`, `Ring b`

Integral Operations

Integral
  (/)         : {a} (Integral a) => a -> a -> a
  (%)         : {a} (Integral a) => a -> a -> a
  (^^)        : {a, e} (Ring a, Integral e) => a -> e -> a
  toInteger   : {a} (Integral a) => a -> Integer
  infFrom     : {a} (Integral a) => a -> [inf]a
  infFromThen : {a} (Integral a) => a -> a -> [inf]a

Instances
Type	Condition
`Integer`
`[n] Bit`	`fin n`

Division

Field
  recip       : {a} (Field a) => a -> a
  (/.)        : {a} (Field a) => a -> a -> a

Instances
Type	Condition
`Rational`
`Z n`	`prime n`
`Float e p`	`ValidFloat e p`

Rounding

Round
  ceiling     : {a} (Round a) => a -> Integer
  floor       : {a} (Round a) => a -> Integer
  trunc       : {a} (Round a) => a -> Integer
  roundAway   : {a} (Round a) => a -> Integer
  roundToEven : {a} (Round a) => a -> Integer

Instances
Type	Condition
`Float e p`	`ValidFloat e p`