Safe Haskell	Safe-Inferred
Language	Haskell2010

Arithmetic.Unsafe

Synopsis

Documentation

newtype Nat (n :: Nat) Source #

A value-level representation of a natural number n.

Constructors

Nat
Fields getNat :: Int

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

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

Finite numbers without the overhead of carrying around a proof.

Constructors

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 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 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 #