Safe Haskell	Safe-Inferred
Language	Haskell2010

Arithmetic.Unsafe

Synopsis

newtype Nat (n :: Nat) = Nat {
- getNat :: Int
}
newtype Nat# :: Nat -> TYPE 'IntRep where
- Nat# :: Int# -> Nat# n
newtype Fin# :: Nat -> TYPE 'IntRep where
- Fin# :: Int# -> Fin# n
newtype MaybeFin# :: Nat -> TYPE 'IntRep where
- MaybeFin# :: Int# -> MaybeFin# n
newtype Fin32# :: Nat -> TYPE 'Int32Rep where
- Fin32# :: Int32# -> Fin32# n
newtype (<#) :: Nat -> Nat -> TYPE ('TupleRep '[]) where
- Lt# :: (# #) -> a <# b
newtype (<=#) :: Nat -> Nat -> TYPE ('TupleRep '[]) where
- Lte# :: (# #) -> a <=# b
data (<) :: Nat -> Nat -> Type where
- Lt :: a < b
data (<=) :: Nat -> Nat -> Type where
- Lte :: a <= b
data (:=:) :: Nat -> Nat -> Type where
- Eq :: a :=: b
newtype (:=:#) :: Nat -> Nat -> TYPE ('TupleRep '[]) where
- Eq# :: (# #) -> 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# :: Nat -> TYPE 'IntRep where Source #

Unboxed variant of Nat.

Constructors

Nat# :: Int# -> Nat# n

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

Finite numbers without the overhead of carrying around a proof.

Constructors

Fin# :: Int# -> Fin# n

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

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

Constructors

MaybeFin# :: Int# -> MaybeFin# n

newtype Fin32# :: Nat -> TYPE 'Int32Rep where Source #

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

Constructors

Fin32# :: Int32# -> Fin32# n

newtype (<#) :: Nat -> Nat -> TYPE ('TupleRep '[]) where infix 4 Source #

Constructors

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

newtype (<=#) :: Nat -> Nat -> TYPE ('TupleRep '[]) where infix 4 Source #

Constructors

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

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

Category (<=) Source #
Instance details Defined in Arithmetic.Unsafe Methods id :: 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

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

newtype (:=:#) :: Nat -> Nat -> TYPE ('TupleRep '[]) where infix 4 Source #

Constructors

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