Safe Haskell	None
Language	Haskell2010

Data.TypeNat.Nat

Synopsis

data Nat
- = Z
- | S Nat
class IsNat (n :: Nat) where
- natRecursion :: (forall m. b -> a m -> a (S m)) -> (b -> a Z) -> (b -> b) -> b -> a n
class LTE (n :: Nat) (m :: Nat) where
- lteInduction :: StrongLTE m l => Proxy l -> (forall k. LTE (S k) l => d k -> d (S k)) -> d n -> d m
- lteRecursion :: (forall k. LTE n k => d (S k) -> d k) -> d m -> d n
type family StrongLTE (n :: Nat) (m :: Nat) :: Constraint where ...
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

Documentation

Natural numbers

Constructors

Z
S Nat

Instances details

Eq Nat Source #
Instance details Defined in Data.TypeNat.Nat Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Ord Nat Source #
Instance details 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 Source #

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

Instances details

IsNat 'Z Source #
Instance details Defined in Data.TypeNat.Nat Methods natRecursion :: (forall (m :: Nat). b -> a m -> a ('S m)) -> (b -> a 'Z) -> (b -> b) -> b -> a 'Z Source #
IsNat n => IsNat ('S n) Source #
Instance details 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) Source #

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

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

Methods

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

Instances details

LTE n n Source #
Instance details 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 Source # lteRecursion :: (forall (k :: Nat). LTE n k => d ('S k) -> d k) -> d n -> d n Source #
LTE n m => LTE n ('S m) Source #
Instance details 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) Source # lteRecursion :: (forall (k :: Nat). LTE n k => d ('S k) -> d k) -> d ('S m) -> d n Source #

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

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)