diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr index 471f13f..2a6f1f2 100644 --- a/src/Quox/Syntax/Shift.idr +++ b/src/Quox/Syntax/Shift.idr @@ -172,3 +172,11 @@ prettyShift bnd by = ||| prints using the `TVar` highlight for variables export PrettyHL (Shift from to) where prettyM = prettyShift TVar + + +infixl 8 // +public export +interface CanShift f where + (//) : f from -> Shift from to -> f to + +export CanShift Var where i // by = shift by i diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr index 34b5b34..f776e86 100644 --- a/src/Quox/Syntax/Subst.idr +++ b/src/Quox/Syntax/Subst.idr @@ -1,6 +1,6 @@ module Quox.Syntax.Subst -import Quox.Syntax.Shift +import public Quox.Syntax.Shift import Quox.Syntax.Var import Quox.Name import Quox.Pretty diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr index 3c0c576..fd0f162 100644 --- a/src/Quox/Syntax/Term.idr +++ b/src/Quox/Syntax/Term.idr @@ -207,6 +207,9 @@ CanSubst (Elim d) (Term d) where s // Shift SZ = s s // th = CloT s th +export CanShift (Term d) where i // by = i // Shift by {env=(Elim d)} +export CanShift (Elim d) where i // by = i // Shift by {env=(Elim d)} + infixl 8 /// mutual