debruijn-safe-0.1: de Bruijn indices and levels
Safe HaskellSafe-Inferred
LanguageHaskell2010

DeBruijn

Synopsis

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

Weakenings, renamings and substitutions

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

Weaken closed term to arbitrary context.

Note: this has different requirements than sinkSize.

Size addition and less-than-equal predicate

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