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

Stabilityexperimental
Maintainerconal@conal.net

TypeUnary.TyNat

Contents

Description

Type-level unary natural numbers

Synopsis

Type-level natural numbers

data Z Source

Type-level representation of zero

Instances

data S n Source

Type-level representation of successor

Instances

IsNat n => IsNat (S n) 

type family a :+: b Source

Sum of type-level numbers

type N0 = ZSource

type N1 = S N0Source

type N2 = S N1Source

type N3 = S N2Source

type N4 = S N3Source

type N5 = S N4Source

type N6 = S N5Source

type N7 = S N6Source

type N8 = S N7Source

type N9 = S N8Source

type N10 = S N9Source

type N11 = S N10Source

type N12 = S N11Source

type N13 = S N12Source

type N14 = S N13Source

type N15 = S N14Source

type N16 = S N15Source