Arithmetic.Types

Documentation

data Nat (n :: Nat)

A value-level representation of a natural number n.

data Difference :: Nat -> Nat -> Type where

Proof that the first argument can be expressed as the sum of the second argument and some other natural number.

Constructors

Difference :: forall a b c. Nat c -> ((c + b) :=: a) -> Difference a b

data Fin :: Nat -> Type where

A finite set of n elements. 'Fin n = { 0 .. n - 1 }'

Constructors

Fin

Fields

• :: { index :: !(Nat m)
•    , proof :: !(m < n)
•    } -> Fin n

Instances

Eq (Fin n)

Defined in Arithmetic.Types

Methods

(==) :: Fin n -> Fin n -> Bool

(/=) :: Fin n -> Fin n -> Bool

Ord (Fin n)

Defined in Arithmetic.Types

Methods

compare :: Fin n -> Fin n -> Ordering

(<) :: Fin n -> Fin n -> Bool

(<=) :: Fin n -> Fin n -> Bool

(>) :: Fin n -> Fin n -> Bool

(>=) :: Fin n -> Fin n -> Bool

max :: Fin n -> Fin n -> Fin n

min :: Fin n -> Fin n -> Fin n

Show (Fin n)

Defined in Arithmetic.Types

Methods

showsPrec :: Int -> Fin n -> ShowS

show :: Fin n -> String

showList :: [Fin n] -> ShowS

data (<) :: Nat -> Nat -> Type infix 4

Proof that the first argument is strictly less than the second argument.

data (<=) :: Nat -> Nat -> Type infix 4

Proof that the first argument is less than or equal to the second argument.

Instances

Category (<=)

Defined in Arithmetic.Unsafe

Methods

id :: a <= a

(.) :: (b <= c) -> (a <= b) -> a <= c

data (:=:) :: Nat -> Nat -> Type infix 4

Proof that the first argument is equal to the second argument.

Instances

Category (:=:)

Defined in Arithmetic.Unsafe

Methods

id :: a :=: a

(.) :: (b :=: c) -> (a :=: b) -> a :=: c