Arithmetic.Unsafe

Documentation

newtype Nat (n :: Nat)

A value-level representation of a natural number n.

Constructors

Nat

Fields

• getNat :: Int

data (<) :: Nat -> Nat -> Type where infix 4

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

Constructors

Lt :: a < b

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

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

Constructors

Lte :: a <= b

Instances

Category (<=)

Defined in Arithmetic.Unsafe

Methods

id :: a <= a

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

data (:=:) :: Nat -> Nat -> Type where infix 4

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

Constructors

Eq :: a :=: b

Instances

Category (:=:)

Defined in Arithmetic.Unsafe

Methods

id :: a :=: a

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