Documentation

data Zero Source #

data Succ n Source #

type N0 = Zero Source #

type N1 = Succ N0 Source #

type P1 w = Succ w Source #

type N2 = Succ N1 Source #

type P2 w = Succ (P1 w) Source #

type N3 = Succ N2 Source #

type P3 w = Succ (P2 w) Source #

type N4 = Succ N3 Source #

type P4 w = Succ (P3 w) Source #

type N5 = Succ N4 Source #

type P5 w = Succ (P4 w) Source #

type N6 = Succ N5 Source #

type P6 w = Succ (P5 w) Source #

type N7 = Succ N6 Source #

type P7 w = Succ (P6 w) Source #

type N8 = Succ N7 Source #

type P8 w = Succ (P7 w) Source #

type N9 = Succ N8 Source #

type P9 w = Succ (P8 w) Source #

type N10 = Succ N9 Source #

type P10 w = Succ (P9 w) Source #

type N11 = Succ N10 Source #

type P11 w = Succ (P10 w) Source #

type N12 = Succ N11 Source #

type P12 w = Succ (P11 w) Source #

n0 :: Size N0 Source #

n1 :: Size N1 Source #

n2 :: Size N2 Source #

n3 :: Size N3 Source #

n4 :: Size N4 Source #

n5 :: Size N5 Source #

n6 :: Size N6 Source #

n7 :: Size N7 Source #

n8 :: Size N8 Source #

n9 :: Size N9 Source #

n10 :: Size N10 Source #

newtype Size n Source #

incSize :: Size n -> Size (Succ n) Source #

class Nat n where Source #

size :: Nat n => Size n Source #

reifyInt :: Int -> (forall n. Nat n => Size n -> a) -> a Source #