debruijn-0.1: de Bruijn indices and levels

Safe Haskell	Safe-Inferred
Language	Haskell2010

DeBruijn.Sub

Contents

Substitution
- Category
Classes

Synopsis

newtype Sub t ctx ctx' = MkSub (Env ctx (t ctx'))
unSub :: Sub t ctx ctx' -> Env ctx (t ctx')
substIdx :: Sub t ctx ctx' -> Idx ctx -> t ctx'
emptySub :: Sub t EmptyCtx ctx'
snocSub :: Sub t ctx ctx' -> t ctx' -> Sub t (S ctx) ctx'
keepSub :: (Renamable t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx')
weakenSub :: Wk ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''
nameMe :: Renamable t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx''
idSub :: Var t => Size ctx -> Sub t ctx ctx
compSub :: Subst t => Sub t ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''
class Var t where
- var :: Idx ctx -> t ctx
class Var t => Subst t where
- subst :: Sub t ctx ctx' -> t ctx -> t ctx'

Substitution

newtype Sub t ctx ctx' Source #

Substitutions.

Constructors

MkSub (Env ctx (t ctx'))

unSub :: Sub t ctx ctx' -> Env ctx (t ctx') Source #

substIdx :: Sub t ctx ctx' -> Idx ctx -> t ctx' Source #

Substitute index.

emptySub :: Sub t EmptyCtx ctx' Source #

Substitution from empty context.

snocSub :: Sub t ctx ctx' -> t ctx' -> Sub t (S ctx) ctx' Source #

keepSub :: (Renamable t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx') Source #

weakenSub :: Wk ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx'' Source #

Precompose Sub with weakening.

nameMe :: Renamable t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx'' Source #

Category

idSub :: Var t => Size ctx -> Sub t ctx ctx Source #

Identity substitution

compSub :: Subst t => Sub t ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx'' Source #

Substitution composition.

Classes

class Var t where Source #

Terms which contain indices as variables.

Methods

var :: Idx ctx -> t ctx Source #

Instances

Instances details

Var Idx Source #
Instance details Defined in DeBruijn.Sub Methods var :: forall (ctx :: Ctx). Idx ctx -> Idx ctx Source #
Var (Proxy :: Ctx -> Type) Source #
Instance details Defined in DeBruijn.Sub Methods var :: forall (ctx :: Ctx). Idx ctx -> Proxy ctx Source #

class Var t => Subst t where Source #

Terms which we can subsitute into.

Methods

subst :: Sub t ctx ctx' -> t ctx -> t ctx' Source #

Instances

Instances details

Subst Idx Source #
Instance details Defined in DeBruijn.Sub Methods subst :: forall (ctx :: Ctx) (ctx' :: Ctx). Sub Idx ctx ctx' -> Idx ctx -> Idx ctx' Source #
Subst (Proxy :: Ctx -> Type) Source #
Instance details Defined in DeBruijn.Sub Methods subst :: forall (ctx :: Ctx) (ctx' :: Ctx). Sub Proxy ctx ctx' -> Proxy ctx -> Proxy ctx' Source #