Modulenatural-arithmetic-0.2.1.0Haskell2010

Arithmetic.Unsafe

11 types

Packagenatural-arithmetic-0.2.1.0
Exports11
LanguageHaskell2010
LicenceBSD-3-Clause
SourceUnsafe.hs

newtypenewtype Nat (n :: Nat)

A value-level representation of a natural number n.

Constructors

Nat
- getNat :: Int

Instances1Show

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

newtypenewtype Nat# (a :: Nat) where

Unboxed variant of Nat.

Constructors

Nat# :: Int# -> Nat# a

newtypenewtype Fin# (a :: Nat) where

Finite numbers without the overhead of carrying around a proof.

Constructors

Fin# :: Int# -> Fin# a

newtypenewtype MaybeFin# (a :: Nat) where

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

Constructors

MaybeFin# :: Int# -> MaybeFin# a

newtypenewtype Fin32# (a :: Nat) where

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

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

Constructors

Lt :: (<) a b

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

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.1.0 · Arithmetic.Unsafe

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

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

Constructors

Eq :: (:=:) a b

Instances1Category

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

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

Constructors

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