Modulenatural-arithmetic-0.2.4.0Haskell2010

Arithmetic.Unsafe

Synopsis

newtype Nat
newtype Nat#
newtype Fin#
newtype MaybeFin#
newtype MaybeFin32#
newtype EitherFin#
newtype Fin32#
newtype <#
newtype <=#
data <
data <=
data :=:
newtype :=:#

Packagenatural-arithmetic-0.2.4.0
Exports13
LanguageHaskell2010
LicenceBSD-3-Clause
SourceUnsafe.hs

newtypenewtype Nat (n :: Nat)

Source#

A value-level representation of a natural number n.

Constructors

Nat
- getNat :: Int

Instances1Show

Show (Nat n)Defined in natural-arithmetic-0.2.4.0 · Arithmetic.Unsafe

newtypenewtype Nat# (a :: Nat) where

Source#

Unboxed variant of Nat.

Constructors

Nat# :: Int# -> Nat# a

newtypenewtype Fin# (a :: Nat) where

Source#

Finite numbers without the overhead of carrying around a proof.

Constructors

Fin# :: Int# -> Fin# a

newtypenewtype MaybeFin# (a :: Nat) where

Source#

Either a Fin# or Nothing. Internally, this uses negative one to mean Nothing.

Constructors

MaybeFin# :: Int# -> MaybeFin# a

newtypenewtype MaybeFin32# (a :: Nat) where

Constructors

MaybeFin32# :: Int32# -> MaybeFin32# a

newtypenewtype EitherFin# (a :: Nat) (b :: Nat) where

Source#

Either a Fin# bounded by the left natural or one bounded by the right natural.

Constructors

EitherFin# :: Int# -> EitherFin# a b

newtypenewtype Fin32# (a :: Nat) where

Source#

Variant of Fin# that only allows 32-bit integers.

Constructors

Fin32# :: Int32# -> Fin32# a

newtypenewtype (<#) (a :: Nat) (b :: Nat) where

Constructors

Lt# :: (# #) -> (<#) a b

newtypenewtype (<=#) (a :: Nat) (b :: Nat) where

Constructors

Lte# :: (# #) -> (<=#) a b

datadata (<) (a :: Nat) (b :: Nat) where

Source#

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

Constructors

Lt :: (<) a b

datadata (<=) (a :: Nat) (b :: Nat) where

Source#

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

Constructors

Lte :: (<=) a b

Instances1Category

Category (<=)Defined in natural-arithmetic-0.2.4.0 · Arithmetic.Unsafe

datadata (:=:) (a :: Nat) (b :: Nat) where

Source#

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

Constructors

Eq :: (:=:) a b

Instances1Category

Category (:=:)Defined in natural-arithmetic-0.2.4.0 · Arithmetic.Unsafe

newtypenewtype (:=:#) (a :: Nat) (b :: Nat) where

Constructors

Eq# :: (# #) -> (:=:#) a b