Safe Haskell	None
Language	Haskell2010

Arithmetic.Types

Contents

Maybe Fin
Either Fin
Infix Operators

Synopsis

data Nat (n :: Nat)
data Nat# (a :: Nat) :: TYPE 'IntRep
data WithNat (a :: Nat -> Type) where
- WithNat :: forall (n :: Nat) (a :: Nat -> Type). !(Nat n) -> a n -> WithNat a
data Difference (a :: Nat) (b :: Nat) where
- Difference :: forall (a :: Nat) (b :: Nat) (c :: Nat). Nat c -> ((c + b) :=: a) -> Difference a b
data Fin (a :: Nat) where
- Fin :: forall (m :: Nat) (a :: Nat). {..} -> Fin a
data Fin# (a :: Nat) :: TYPE 'IntRep
data Fin32# (a :: Nat) :: TYPE 'Int32Rep
data MaybeFin# (a :: Nat) :: TYPE 'IntRep
pattern MaybeFinJust# :: Fin# n -> MaybeFin# n
pattern MaybeFinNothing# :: MaybeFin# n
data EitherFin# (a :: Nat) (b :: Nat) :: TYPE 'IntRep
pattern EitherFinLeft# :: Fin# m -> EitherFin# m n
pattern EitherFinRight# :: Fin# n -> EitherFin# m n
data (a :: Nat) < (b :: Nat)
data (a :: Nat) <= (b :: Nat)
data (a :: Nat) <# (b :: Nat) :: ZeroBitType
data (a :: Nat) <=# (b :: Nat) :: ZeroBitType
data (a :: Nat) :=: (b :: Nat)
data (a :: Nat) :=:# (b :: Nat) :: ZeroBitType

Documentation

data Nat (n :: Nat) Source #

A value-level representation of a natural number n.

Instances

Instances details

Show (Nat n) Source #
Instance details Defined in Arithmetic.Unsafe Methods showsPrec :: Int -> Nat n -> ShowS # show :: Nat n -> String # showList :: [Nat n] -> ShowS #

data Nat# (a :: Nat) :: TYPE 'IntRep Source #

Unboxed variant of Nat.

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

Constructors

WithNat :: forall (n :: Nat) (a :: Nat -> Type). !(Nat n) -> a n -> WithNat a

data Difference (a :: Nat) (b :: Nat) 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 :: Nat) (b :: Nat) (c :: Nat). Nat c -> ((c + b) :=: a) -> Difference a b

data Fin (a :: Nat) where Source #

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

Constructors

Fin
Fields :: forall (m :: Nat) (a :: Nat). { index :: !(Nat m) , proof :: !(m < a) } -> Fin a

Instances

Instances details

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

data Fin# (a :: Nat) :: TYPE 'IntRep Source #

Finite numbers without the overhead of carrying around a proof.

data Fin32# (a :: Nat) :: TYPE 'Int32Rep Source #

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

Maybe Fin

data MaybeFin# (a :: Nat) :: TYPE 'IntRep Source #

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

pattern MaybeFinJust# :: Fin# n -> MaybeFin# n Source #

pattern MaybeFinNothing# :: MaybeFin# n Source #

Either Fin

data EitherFin# (a :: Nat) (b :: Nat) :: TYPE 'IntRep Source #

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

pattern EitherFinLeft# :: Fin# m -> EitherFin# m n Source #

pattern EitherFinRight# :: Fin# n -> EitherFin# m n Source #

Infix Operators

data (a :: Nat) < (b :: Nat) infix 4 Source #

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

data (a :: Nat) <= (b :: Nat) infix 4 Source #

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

Instances

Instances details

Category (<=) Source #
Instance details Defined in Arithmetic.Unsafe Methods id :: forall (a :: Nat). a <= a # (.) :: forall (b :: Nat) (c :: Nat) (a :: Nat). (b <= c) -> (a <= b) -> a <= c #

data (a :: Nat) <# (b :: Nat) :: ZeroBitType infix 4 Source #

data (a :: Nat) <=# (b :: Nat) :: ZeroBitType infix 4 Source #

data (a :: Nat) :=: (b :: Nat) infix 4 Source #

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

Instances

Instances details

Category (:=:) Source #
Instance details Defined in Arithmetic.Unsafe Methods id :: forall (a :: Nat). a :=: a # (.) :: forall (b :: Nat) (c :: Nat) (a :: Nat). (b :=: c) -> (a :=: b) -> a :=: c #

data (a :: Nat) :=:# (b :: Nat) :: ZeroBitType infix 4 Source #