TypeNat-0.5.0.0: Some Nat-indexed types for GHC

Safe HaskellNone
LanguageHaskell2010

Data.TypeNat.Nat

Synopsis

Documentation

data Nat Source #

Natural numbers

Constructors

Z 
S Nat 

Instances

Eq Nat Source # 

Methods

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

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

Ord Nat Source # 

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

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

Minimal complete definition

natRecursion

Methods

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

Instances

IsNat Z Source # 

Methods

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

IsNat n => IsNat (S n) Source # 

Methods

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

class LTE n m where Source #

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

Minimal complete definition

lteInduction, lteRecursion

Methods

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

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

Instances

LTE n n Source # 

Methods

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

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

LTE n m => LTE n (S m) Source # 

Methods

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

lteRecursion :: (forall k. 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) 

type Zero = Z Source #

type One = S Z Source #

type Two = S One Source #

type Three = S Two Source #

type Five = S Four Source #

type Six = S Five Source #

type Seven = S Six Source #

type Ten = S Nine Source #