type-unary-0.1.16: Type-level and typed unary natural numbers, inequality proofs, vectors
TypeUnary.TyNat
Contents
Description
Type-level unary natural numbers
Synopsis
data Z Source
Type-level representation of zero
Instances
data S n Source
Type-level representation of successor
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