DeBruijn

Basic building blocks

data Ctx  :: Kind                   -- contexts
data Idx  :: Ctx -> Type            -- de Bruijn indices
data Env  :: Ctx -> Type -> Type    -- environments
data Lvl  :: Ctx -> Type            -- de Bruijn levels
data Size :: Ctx -> Type            -- context size

module DeBruijn.Ctx

module DeBruijn.Idx

module DeBruijn.Env

module DeBruijn.Lvl

module DeBruijn.Size

Weakenings, renamings and substitutions

module DeBruijn.Wk

module DeBruijn.Ren

module DeBruijn.Sub

weakenUsingSize :: Renamable t => Size ctx -> t EmptyCtx -> t ctx

Weaken closed term to arbitrary context.

Note: this has different requirements than sinkSize.

Size addition and less-than-equal predicate

module DeBruijn.Add

Module DeBruijn.Lte is not exported, as it's not that useful in general.