debruijn-0.3.1: de Bruijn indices and levels

Safe Haskell	None
Language	Haskell2010

DeBruijn

Contents

Synopsis

module DeBruijn.Ctx
module DeBruijn.Idx
module DeBruijn.Env
module DeBruijn.Lvl
module DeBruijn.Size
module DeBruijn.Wk
module DeBruijn.Ren
module DeBruijn.Sub
weakenUsingSize :: forall t (ctx :: Ctx). Weaken t => Size ctx -> t EmptyCtx -> t ctx
module DeBruijn.Add

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 :: forall t (ctx :: Ctx). Weaken 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.Add

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