type-unary-0.3.2: Type-level and typed unary natural numbers, inequality proofs, vectors

Copyright(c) Conal Elliott 2009
LicenseBSD3
Maintainerconal@conal.net
Stabilityexperimental
Safe HaskellSafe
LanguageHaskell98

TypeUnary.TyNat

Contents

Description

Type-level unary natural numbers

Synopsis

Type-level natural numbers

data Z Source #

Type-level representation of zero

Instances

IsNat Z Source # 

Methods

nat :: Nat Z Source #

Newtype (Vec Z a) # 

Associated Types

type O (Vec Z a) :: * #

Methods

pack :: O (Vec Z a) -> Vec Z a #

unpack :: Vec Z a -> O (Vec Z a) #

type n :-: Z Source # 
type n :-: Z = n
type Z :*: b Source # 
type Z :*: b = Z
type Z :+: b Source # 
type Z :+: b = b
type O (Vec Z a) # 
type O (Vec Z a) = ()

data S n Source #

Type-level representation of successor

Instances

IsNat n => IsNat (S n) Source # 

Methods

nat :: Nat (S n) Source #

Newtype (Vec (S n) a) # 

Associated Types

type O (Vec (S n) a) :: * #

Methods

pack :: O (Vec (S n) a) -> Vec (S n) a #

unpack :: Vec (S n) a -> O (Vec (S n) a) #

type (S a) :*: b Source # 
type (S a) :*: b = (:+:) b ((:*:) a b)
type (S a) :+: b Source # 
type (S a) :+: b = S ((:+:) a b)
type (S n) :-: (S m) Source # 
type (S n) :-: (S m) = (:-:) n m
type O (Vec (S n) a) # 
type O (Vec (S n) a) = (a, Vec n a)

type family a :+: b infixl 6 Source #

Sum of type-level numbers

Instances

type Z :+: b Source # 
type Z :+: b = b
type (S a) :+: b Source # 
type (S a) :+: b = S ((:+:) a b)

type family a :*: b infixl 7 Source #

Product of type-level numbers

Instances

type Z :*: b Source # 
type Z :*: b = Z
type (S a) :*: b Source # 
type (S a) :*: b = (:+:) b ((:*:) a b)

type family a :-: b infixl 6 Source #

Instances

type n :-: Z Source # 
type n :-: Z = n
type (S n) :-: (S m) Source # 
type (S n) :-: (S m) = (:-:) n m

type N0 = Z Source #

type N1 = S N0 Source #

type N2 = S N1 Source #

type N3 = S N2 Source #

type N4 = S N3 Source #

type N5 = S N4 Source #

type N6 = S N5 Source #

type N7 = S N6 Source #

type N8 = S N7 Source #

type N9 = S N8 Source #

type N10 = S N9 Source #

type N11 = S N10 Source #

type N12 = S N11 Source #

type N13 = S N12 Source #

type N14 = S N13 Source #

type N15 = S N14 Source #

type N16 = S N15 Source #