Safe Haskell	None
Language	Haskell2010

Arithmetic.Unsafe

Synopsis

newtype Nat (n :: Nat) = Nat {
- getNat :: Int
}
newtype Nat# (a :: Nat) :: TYPE 'IntRep where
- Nat# :: forall (a :: Nat). Int# -> Nat# a
newtype Fin# (a :: Nat) :: TYPE 'IntRep where
- Fin# :: forall (a :: Nat). Int# -> Fin# a
newtype MaybeFin# (a :: Nat) :: TYPE 'IntRep where
- MaybeFin# :: forall (a :: Nat). Int# -> MaybeFin# a
newtype EitherFin# (a :: Nat) (b :: Nat) :: TYPE 'IntRep where
- EitherFin# :: forall (a :: Nat) (b :: Nat). Int# -> EitherFin# a b
newtype Fin32# (a :: Nat) :: TYPE 'Int32Rep where
- Fin32# :: forall (a :: Nat). Int32# -> Fin32# a
newtype (a :: Nat) <# (b :: Nat) :: ZeroBitType where
- Lt# :: forall (a :: Nat) (b :: Nat). (# #) -> a <# b
newtype (a :: Nat) <=# (b :: Nat) :: ZeroBitType where
- Lte# :: forall (a :: Nat) (b :: Nat). (# #) -> a <=# b
data (a :: Nat) < (b :: Nat) where
- Lt :: forall (a :: Nat) (b :: Nat). a < b
data (a :: Nat) <= (b :: Nat) where
- Lte :: forall (a :: Nat) (b :: Nat). a <= b
data (a :: Nat) :=: (b :: Nat) where
- Eq :: forall (a :: Nat) (b :: Nat). a :=: b
newtype (a :: Nat) :=:# (b :: Nat) :: ZeroBitType where
- Eq# :: forall (a :: Nat) (b :: Nat). (# #) -> a :=:# b

Documentation

newtype Nat (n :: Nat) Source #

A value-level representation of a natural number n.

Constructors

Nat
Fields getNat :: Int

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 #

newtype Nat# (a :: Nat) :: TYPE 'IntRep where Source #

Unboxed variant of Nat.

Constructors

Nat# :: forall (a :: Nat). Int# -> Nat# a

newtype Fin# (a :: Nat) :: TYPE 'IntRep where Source #

Finite numbers without the overhead of carrying around a proof.

Constructors

Fin# :: forall (a :: Nat). Int# -> Fin# a

newtype MaybeFin# (a :: Nat) :: TYPE 'IntRep where Source #

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

Constructors

MaybeFin# :: forall (a :: Nat). Int# -> MaybeFin# a

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

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

Constructors

EitherFin# :: forall (a :: Nat) (b :: Nat). Int# -> EitherFin# a b

newtype Fin32# (a :: Nat) :: TYPE 'Int32Rep where Source #

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

Constructors

Fin32# :: forall (a :: Nat). Int32# -> Fin32# a

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

Constructors

Lt# :: forall (a :: Nat) (b :: Nat). (# #) -> a <# b

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

Constructors

Lte# :: forall (a :: Nat) (b :: Nat). (# #) -> a <=# b

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

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

Constructors

Lt :: forall (a :: Nat) (b :: Nat). a < b

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

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

Constructors

Lte :: forall (a :: Nat) (b :: Nat). a <= b

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) where infix 4 Source #

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

Constructors

Eq :: forall (a :: Nat) (b :: Nat). a :=: b

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 #

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

Constructors

Eq# :: forall (a :: Nat) (b :: Nat). (# #) -> a :=:# b