TypeLevelNat
Synopsis
data Z = Z
newtype S n = S n
class Nat n where
 caseNat :: forall r. n -> (n ~ Z => r) -> (forall p. (n ~ S p, Nat p) => p -> r) -> r
induction :: forall p n. Nat n => n -> p Z -> (forall m. Nat m => p m -> p (S m)) -> p n
witnessNat :: forall n. Nat n => n
data N n where
 Zero :: N Z Succ :: N n -> N (S n)
nat :: forall n. Nat n => n -> N n
Documentation
 data Z Source
Type-level natural denoting zero
Constructors
 Z
Instances
 Show Z Nat Z ComposeN Z
 newtype S n Source
Type-level natural denoting the Successor of another type-level natural.
Constructors
 S n
Instances
 Show n => Show (S n) Nat p => Nat (S p) ComposeN n => ComposeN (S n)
 class Nat n where Source
Class of all type-level naturals.
Methods
 caseNat Source
 :: forall r . => n The natural number to case analyse. -> n ~ Z => r The result r when n equals zero. -> forall p. (n ~ S p, Nat p) => p -> r Function to apply to the predecessor of n to yield the result r. -> r Case analysis on natural numbers.
Instances
 Nat Z Nat p => Nat (S p)
 induction :: forall p n. Nat n => n -> p Z -> (forall m. Nat m => p m -> p (S m)) -> p n Source
The axiom of induction on natural numbers. See: http://en.wikipedia.org/wiki/Mathematical_induction#Axiom_of_induction
 witnessNat :: forall n. Nat n => n Source

The value of witnessNat :: n is the natural number of type n. For example:

``` *TypeLevelNat> witnessNat :: S (S (S Z))
S (S (S Z))
```
 data N n where Source
A value-level natural indexed with an equivalent type-level natural.
Constructors
 Zero :: N Z Succ :: N n -> N (S n)
 nat :: forall n. Nat n => n -> N n Source
Produced by Haddock version 2.4.2