DeBruijn.Sub

Substitution

newtype Sub t ctx ctx'

Substitutions.

Constructors

MkSub (Env ctx (t ctx'))

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

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

Substitute index.

emptySub :: Sub t EmptyCtx ctx'

Substitution from empty context.

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

keepSub :: (Rename 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''

Precompose Sub with weakening.

nameMe :: Rename t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx''

Category

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

Identity substitution

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

Substitution composition.

Classes

class Var t where

Terms which contain indices as variables.

Methods

var :: Idx ctx -> t ctx

Instances

Var Idx

Defined in DeBruijn.Sub

Methods

var :: forall (ctx :: Ctx). Idx ctx -> Idx ctx

Var (Proxy :: Ctx -> Type)

Defined in DeBruijn.Sub

Methods

var :: forall (ctx :: Ctx). Idx ctx -> Proxy ctx

class Var t => Subst t where

Terms which we can subsitute into.

Methods

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

Instances

Subst Idx

Defined in DeBruijn.Sub

Methods

subst :: forall (ctx :: Ctx) (ctx' :: Ctx). Sub Idx ctx ctx' -> Idx ctx -> Idx ctx'

Subst (Proxy :: Ctx -> Type)

Defined in DeBruijn.Sub

Methods

subst :: forall (ctx :: Ctx) (ctx' :: Ctx). Sub Proxy ctx ctx' -> Proxy ctx -> Proxy ctx'