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 #
Methods testEquality :: f a -> f b -> Maybe ((Nat :~: a) b) #
Read1 N Nat Source #
Methods readsPrec1 :: Int -> ReadS (Some Nat f) Source #
Show1 N Nat Source #
Methods showsPrec1 :: Int -> f a -> ShowS Source # show1 :: f a -> String Source #
Ord1 N Nat Source #
Methods compare1 :: f a -> f a -> Ordering Source # (<#) :: f a -> f a -> Bool Source # (>#) :: f a -> f a -> Bool Source # (<=#) :: f a -> f a -> Bool Source # (>=#) :: f a -> f a -> Bool Source #
Eq1 N Nat Source #
Methods eq1 :: f a -> f a -> Bool Source # neq1 :: f a -> f a -> Bool Source #
BoolEquality N Nat Source #
Methods boolEquality :: f a -> f b -> Boolean ((Nat == a) b) Source #
Known N Nat Z Source #	`Z_` is the canonical construction of a `Nat Z`.
Associated Types type KnownC Nat (Z :: Nat -> *) (a :: Nat) :: Constraint Source # Methods known :: Z a Source #
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)`.
Associated Types type KnownC Nat (S n :: Nat -> *) (a :: Nat) :: Constraint Source # Methods known :: S n a Source #
(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source #
Associated Types type WitnessC (ØC :: Constraint) ((Known N Nat n, Known [k] (Length k) as) :: Constraint) (Length k as) :: Constraint Source # Methods (\\) :: ØC => ((Known N Nat n, Known [k] (Length k) as) -> r) -> Length k as -> r Source #
Witness ØC (Known N Nat n) (Nat n) Source #	A `Nat n` is a `Witness` that there is a canonical construction for `Nat n`.
Associated Types type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (Nat n) :: Constraint Source # Methods (\\) :: ØC => (Known N Nat n -> r) -> Nat n -> r Source #
Witness ØC (Known N Nat n) (VecT k n f a) Source #
Associated Types type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (VecT k n f a) :: Constraint Source # Methods (\\) :: ØC => (Known N Nat n -> r) -> VecT k n f a -> r Source #
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x)) => Witness ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) Source #
Associated Types type WitnessC (ØC :: Constraint) (((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) :: Constraint) (NatGT x y) :: Constraint Source # Methods (\\) :: ØC => (((N ~ x) (S x'), Known N Nat y, (Bool ~ lt) False, (Bool ~ eq) False, (Bool ~ gt) True) -> r) -> NatGT x y -> r Source #
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y)) => Witness ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) Source #
Associated Types type WitnessC (ØC :: Constraint) (((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) :: Constraint) (NatEQ x y) :: Constraint Source # Methods (\\) :: ØC => (((N ~ x) y, Known N Nat x, (Bool ~ lt) False, (Bool ~ eq) True, (Bool ~ gt) False) -> r) -> NatEQ x y -> r Source #
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y)) => Witness ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) Source #
Associated Types type WitnessC (ØC :: Constraint) (((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) :: Constraint) (NatLT x y) :: Constraint Source # Methods (\\) :: ØC => (((N ~ y) (S y'), Known N Nat x, (Bool ~ lt) True, (Bool ~ eq) False, (Bool ~ gt) False) -> r) -> NatLT x y -> r Source #
Eq (Nat n) Source #
Methods (==) :: Nat n -> Nat n -> Bool # (/=) :: Nat n -> Nat n -> Bool #
Ord (Nat n) Source #
Methods compare :: Nat n -> Nat n -> Ordering # (<) :: Nat n -> Nat n -> Bool # (<=) :: Nat n -> Nat n -> Bool # (>) :: Nat n -> Nat n -> Bool # (>=) :: Nat n -> Nat n -> Bool # max :: Nat n -> Nat n -> Nat n # min :: Nat n -> Nat n -> Nat n #
Show (Nat n) Source #
Methods showsPrec :: Int -> Nat n -> ShowS # show :: Nat n -> String # showList :: [Nat n] -> ShowS #
type KnownC N Nat Z Source #
type KnownC N Nat Z = ØC
type KnownC N Nat (S n) Source #
type KnownC N Nat (S n) = Known N Nat n
type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source #
type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) = (~) N n (Len k as)
type WitnessC ØC (Known N Nat n) (Nat n) Source #
type WitnessC ØC (Known N Nat n) (Nat n) = ØC
type WitnessC ØC (Known N Nat n) (VecT k n f a) Source #
type WitnessC ØC (Known N Nat n) (VecT k n f a) = ØC
type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) Source #
type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x))
type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) Source #
type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y))
type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) Source #
type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y))

pred' :: Nat (S x) -> Nat x Source #

onNatPred :: (Nat x -> Nat y) -> Nat (S x) -> Nat (S y) Source #

_Z :: Z :~: Z Source #

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

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

_ZneS :: (Z :~: S x) -> Void 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 #

natVal :: Nat n -> Int Source #