natural-arithmetic-0.1.2.0: Arithmetic of natural numbers

Safe HaskellNone
LanguageHaskell2010

Arithmetic.Unsafe

Synopsis

Documentation

newtype Nat (n :: Nat) Source #

A value-level representation of a natural number n.

Constructors

Nat 

Fields

Instances
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 -> 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
Category (<=) Source # 
Instance details

Defined in Arithmetic.Unsafe

Methods

id :: a <= a #

(.) :: (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
Category (:=:) Source # 
Instance details

Defined in Arithmetic.Unsafe

Methods

id :: a :=: a #

(.) :: (b :=: c) -> (a :=: b) -> a :=: c #