Language.Glambda.Shift

de Bruijn shifting and substitution

Documentation

shift :: forall ts2 t ty. Exp ts2 ty -> Exp (t : ts2) ty

Convert an expression typed in one context to one typed in a larger context. Operationally, this amounts to de Bruijn index shifting. As a proposition, this is the weakening lemma.

subst :: forall ts2 s t. Exp ts2 s -> Exp (s : ts2) t -> Exp ts2 t

Substitute the first expression into the second. As a proposition, this is the substitution lemma.