natural-arithmetic-0.1.2.0: Arithmetic of natural numbers

Arithmetic.Types

Synopsis

Documentation

data Nat (n :: Nat) Source #

A value-level representation of a natural number n.

Instances
 Show (Nat n) Source # Instance detailsDefined in Arithmetic.Unsafe MethodsshowsPrec :: Int -> Nat n -> ShowS #show :: Nat n -> String #showList :: [Nat n] -> ShowS #

data WithNat :: (Nat -> Type) -> Type where Source #

Constructors

 WithNat :: !(Nat n) -> f n -> WithNat f

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

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 Source #

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) Source # Instance detailsDefined in Arithmetic.Types Methods(==) :: Fin n -> Fin n -> Bool #(/=) :: Fin n -> Fin n -> Bool # Ord (Fin n) Source # Instance detailsDefined in Arithmetic.Types Methodscompare :: 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) Source # Instance detailsDefined in Arithmetic.Types MethodsshowsPrec :: Int -> Fin n -> ShowS #show :: Fin n -> String #showList :: [Fin n] -> ShowS #

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

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

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

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

Instances
 Source # Instance detailsDefined in Arithmetic.Unsafe Methodsid :: a <= a #(.) :: (b <= c) -> (a <= b) -> a <= c #

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

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

Instances
 Source # Instance detailsDefined in Arithmetic.Unsafe Methodsid :: a :=: a #(.) :: (b :=: c) -> (a :=: b) -> a :=: c #