DeBruijn.Ctx
type Ctx = Nat Source #
Context counts variables, in other words context is just a natural number.
type EmptyCtx = Z Source #
Empty context is zero.
type S = 'S Source #
And context extension is a successor.
type Ctx1 = S EmptyCtx Source #
type Ctx2 = S Ctx1 Source #
type Ctx3 = S Ctx2 Source #
type Ctx4 = S Ctx3 Source #
type Ctx5 = S Ctx4 Source #
type Ctx6 = S Ctx5 Source #
type Ctx7 = S Ctx6 Source #
type Ctx8 = S Ctx7 Source #
type Ctx9 = S Ctx8 Source #