add CanShift interface like CanSubst

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

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

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