Data.TypeNat.Nat

Documentation

data Nat

Natural numbers

Constructors

Z

S Nat

Instances

Eq Nat

Defined in Data.TypeNat.Nat

Methods

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

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

Ord Nat

Defined in Data.TypeNat.Nat

Methods

compare :: Nat -> Nat -> Ordering

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

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

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

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

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

class IsNat (n :: Nat) where

Proof that a given type is a Nat. With this fact, you can do type-directed computation.

Methods

natRecursion :: (forall m. b -> a m -> a (S m)) -> (b -> a Z) -> (b -> b) -> b -> a n

Instances

IsNat 'Z

Defined in Data.TypeNat.Nat

Methods

natRecursion :: (forall (m :: Nat). b -> a m -> a ('S m)) -> (b -> a 'Z) -> (b -> b) -> b -> a 'Z

IsNat n => IsNat ('S n)

Defined in Data.TypeNat.Nat

Methods

natRecursion :: (forall (m :: Nat). b -> a m -> a ('S m)) -> (b -> a 'Z) -> (b -> b) -> b -> a ('S n)

class LTE (n :: Nat) (m :: Nat) where

Nat n is less than or equal to nat m. Comes with functions to do type-directed computation for Nat-indexed datatypes.

Methods

lteInduction

Arguments

:: StrongLTE m l

=> Proxy l

-> (forall k. LTE (S k) l => d k -> d (S k))

The parameter l is fixed by any call to lteInduction, but due to the StrongLTE m l constraint, we have LTE j l for every j <= m. This allows us to implement the nontrivial case in the LTE p q => LTE p (S q) instance, where we need to use this function to get x :: d p and then again to get f x :: d (S p). So long as p and S p are both less or equal to l, this can be done.

-> d n

-> d m

lteRecursion :: (forall k. LTE n k => d (S k) -> d k) -> d m -> d n

Instances

LTE n n

Defined in Data.TypeNat.Nat

Methods

lteInduction :: forall (l :: Nat) d. StrongLTE n l => Proxy l -> (forall (k :: Nat). LTE ('S k) l => d k -> d ('S k)) -> d n -> d n

lteRecursion :: (forall (k :: Nat). LTE n k => d ('S k) -> d k) -> d n -> d n

LTE n m => LTE n ('S m)

Defined in Data.TypeNat.Nat

Methods

lteInduction :: forall (l :: Nat) d. StrongLTE ('S m) l => Proxy l -> (forall (k :: Nat). LTE ('S k) l => d k -> d ('S k)) -> d n -> d ('S m)

lteRecursion :: (forall (k :: Nat). LTE n k => d ('S k) -> d k) -> d ('S m) -> d n

type family StrongLTE (n :: Nat) (m :: Nat) :: Constraint where ...

A constrint which includes LTE k m for every k <= m.

Equations

StrongLTE Z m = LTE Z m

StrongLTE (S n) m = (LTE (S n) m, StrongLTE n m)

type Zero = Z

type One = S Z

type Two = S One

type Three = S Two

type Four = S Three

type Five = S Four

type Six = S Five

type Seven = S Six

type Eight = S Seven

type Nine = S Eight

type Ten = S Nine