Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Data.Type.Nat

Description

A singleton-esque type for representing Peano natural numbers.

Synopsis

Documentation

data Nat :: N -> * where Source

Constructors

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

Instances

TestEquality N Nat Source
Read1 N Nat Source
Show1 N Nat Source
Ord1 N Nat Source
Eq1 N Nat Source
Known N Nat Z Source	`Z_` is the canonical construction of a `Nat Z`.
Known N Nat n => Known N Nat (S n) Source	If `n` is a canonical construction of `Nat n`, `S_ n` is the canonical construction of `Nat (S n)`.
Witness ØC (Known N Nat n) (Nat n) Source	A `Nat n` is a `Witness` that there is a canonical construction for `Nat n`.
Witness ØC (Known N Nat n) (VT k n f a) Source
Eq (Nat n) Source
Ord (Nat n) Source
Show (Nat n) Source
type KnownC N Nat Z = ØC
type KnownC N Nat (S n) = Known N Nat n Source
type WitnessC ØC (Known N Nat n) (Nat n) = ØC
type WitnessC ØC (Known N Nat n) (VT k n f a) = ØC

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

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

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

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

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

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

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

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