Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 :: Rename t => Size ctx -> t EmptyCtx -> t ctx
- module DeBruijn.Add
Basic building blocks
dataCtx
:: Kind -- contexts dataIdx
::Ctx
-> Type -- de Bruijn indices dataEnv
::Ctx
-> Type -> Type -- environments dataLvl
::Ctx
-> Type -- de Bruijn levels dataSize
::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 :: Rename 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.