natural-arithmetic-0.1.3.0: Arithmetic of natural numbers

Arithmetic.Unsafe

Synopsis

Documentation

newtype Nat (n :: Nat) Source #

A value-level representation of a natural number n.

Constructors

 Nat FieldsgetNat :: Int

Instances

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

newtype Fin# :: Nat -> TYPE 'IntRep where Source #

Finite numbers without the overhead of carrying around a proof.

Constructors

 Fin# :: Int# -> Fin# n

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

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

Constructors

 Lt :: a < b

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

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

Constructors

 Lte :: a <= b

Instances

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

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

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

Constructors

 Eq :: a :=: b

Instances

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