Safe Haskell	Safe-Inferred
Language	Haskell2010

Arithmetic.Types

Synopsis

data Nat (n :: Nat)
data Nat# :: Nat -> TYPE 'IntRep
data WithNat :: (Nat -> Type) -> Type where
- WithNat :: !(Nat n) -> f n -> WithNat f
data Difference :: Nat -> Nat -> Type where
- Difference :: forall a b c. Nat c -> ((c + b) :=: a) -> Difference a b
data Fin :: Nat -> Type where
- Fin :: forall m n. {..} -> Fin n
data Fin# :: Nat -> TYPE 'IntRep
data (<) :: Nat -> Nat -> Type
data (<=) :: Nat -> Nat -> Type
data (:=:) :: Nat -> Nat -> Type

Documentation

data Nat (n :: Nat) Source #

A value-level representation of a natural number n.

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 #

Unboxed variant of Nat.

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

Constructors

WithNat :: !(Nat n) -> f n -> WithNat f

Proof that the first argument can be expressed as the sum of the second argument and some other natural number.

Constructors

Difference :: forall a b c. Nat c -> ((c + b) :=: a) -> Difference a b

data Fin :: Nat -> Type where Source #

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

Constructors

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

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 #

Finite numbers without the overhead of carrying around a proof.

data (<) :: Nat -> Nat -> Type infix 4 Source #

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

data (<=) :: Nat -> Nat -> Type infix 4 Source #

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

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

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

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 #