From a2be5a468dac87c252d67ea002d69cb35ecc08f4 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 9 Sep 2021 23:53:00 +0200
Subject: [PATCH] add CanShift interface like CanSubst

---
 src/Quox/Syntax/Shift.idr | 8 ++++++++
 src/Quox/Syntax/Subst.idr | 2 +-
 src/Quox/Syntax/Term.idr  | 3 +++
 3 files changed, 12 insertions(+), 1 deletion(-)

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