Data.Type.Nat

A singleton-esque type for representing Peano natural numbers.

Documentation

data Nat :: N -> * where

Constructors

Z_ :: Nat Z

S_ :: !(Nat n) -> Nat (S n)

Instances

TestEquality N Nat

Methods

testEquality :: f a -> f b -> Maybe ((Nat :~: a) b)

Read1 N Nat

Methods

readsPrec1 :: Int -> ReadS (Some Nat f)

Show1 N Nat

Methods

showsPrec1 :: Int -> f a -> ShowS

show1 :: f a -> String

Ord1 N Nat

Methods

compare1 :: f a -> f a -> Ordering

(<#) :: f a -> f a -> Bool

(>#) :: f a -> f a -> Bool

(<=#) :: f a -> f a -> Bool

(>=#) :: f a -> f a -> Bool

Eq1 N Nat

Methods

eq1 :: f a -> f a -> Bool

neq1 :: f a -> f a -> Bool

BoolEquality N Nat

Methods

boolEquality :: f a -> f b -> Boolean ((Nat == a) b)

Known N Nat Z

Z_ is the canonical construction of a Nat Z.

Associated Types

type KnownC Nat (Z :: Nat -> *) (a :: Nat) :: Constraint

Methods

known :: Z a

Known N Nat n => Known N Nat (S n)

If n is a canonical construction of Nat n, S_ n is the canonical construction of Nat (S n).

Associated Types

type KnownC Nat (S n :: Nat -> *) (a :: Nat) :: Constraint

Methods

known :: S n a

(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as)

Associated Types

type WitnessC (ØC :: Constraint) ((Known N Nat n, Known [k] (Length k) as) :: Constraint) (Length k as) :: Constraint

Methods

(\\) :: ØC => ((Known N Nat n, Known [k] (Length k) as) -> r) -> Length k as -> r

Witness ØC (Known N Nat n) (Nat n)

A Nat n is a Witness that there is a canonical construction for Nat n.

Associated Types

type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (Nat n) :: Constraint

Methods

(\\) :: ØC => (Known N Nat n -> r) -> Nat n -> r

Witness ØC (Known N Nat n) (VecT k n f a)

Associated Types

type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (VecT k n f a) :: Constraint

Methods

(\\) :: ØC => (Known N Nat n -> r) -> VecT k n f a -> r

((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x)) => Witness ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y)

Associated Types

type WitnessC (ØC :: Constraint) (((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) :: Constraint) (NatGT x y) :: Constraint

Methods

(\\) :: ØC => (((N ~ x) (S x'), Known N Nat y, (Bool ~ lt) False, (Bool ~ eq) False, (Bool ~ gt) True) -> r) -> NatGT x y -> r

((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y)) => Witness ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y)

Associated Types

type WitnessC (ØC :: Constraint) (((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) :: Constraint) (NatEQ x y) :: Constraint

Methods

(\\) :: ØC => (((N ~ x) y, Known N Nat x, (Bool ~ lt) False, (Bool ~ eq) True, (Bool ~ gt) False) -> r) -> NatEQ x y -> r

((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y)) => Witness ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y)

Associated Types

type WitnessC (ØC :: Constraint) (((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) :: Constraint) (NatLT x y) :: Constraint

Methods

(\\) :: ØC => (((N ~ y) (S y'), Known N Nat x, (Bool ~ lt) True, (Bool ~ eq) False, (Bool ~ gt) False) -> r) -> NatLT x y -> r

Eq (Nat n)

Methods

(==) :: Nat n -> Nat n -> Bool

(/=) :: Nat n -> Nat n -> Bool

Ord (Nat n)

Methods

compare :: Nat n -> Nat n -> Ordering

(<) :: Nat n -> Nat n -> Bool

(<=) :: Nat n -> Nat n -> Bool

(>) :: Nat n -> Nat n -> Bool

(>=) :: Nat n -> Nat n -> Bool

max :: Nat n -> Nat n -> Nat n

min :: Nat n -> Nat n -> Nat n

Show (Nat n)

Methods

showsPrec :: Int -> Nat n -> ShowS

show :: Nat n -> String

showList :: [Nat n] -> ShowS

type KnownC N Nat Z

type KnownC N Nat Z = ØC

type KnownC N Nat (S n)

type KnownC N Nat (S n) = Known N Nat n

type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as)

type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) = (~) N n (Len k as)

type WitnessC ØC (Known N Nat n) (Nat n)

type WitnessC ØC (Known N Nat n) (Nat n) = ØC

type WitnessC ØC (Known N Nat n) (VecT k n f a)

type WitnessC ØC (Known N Nat n) (VecT k n f a) = ØC

type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y)

type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x))

type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y)

type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y))

type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y)

type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y))

pred' :: Nat (S x) -> Nat x

onNatPred :: (Nat x -> Nat y) -> Nat (S x) -> Nat (S y)

_Z :: Z :~: Z

_S :: (x :~: y) -> S x :~: S y

_s :: (S x :~: S y) -> x :~: y

_ZneS :: (Z :~: S x) -> Void

addZ :: Nat x -> (x + Z) :~: x

A proof that Z is also a right identity for the addition of type-level Nats.

addS :: Nat x -> Nat y -> S (x + y) :~: (x + S y)

(.+) :: Nat x -> Nat y -> Nat (x + y) infixr 6

(.*) :: Nat x -> Nat y -> Nat (x * y) infixr 7

(.^) :: Nat x -> Nat y -> Nat (x ^ y) infixl 8

elimNat :: p Z -> (forall x. Nat x -> p x -> p (S x)) -> Nat n -> p n

natVal :: Nat n -> Int