From 7bc58625a115460c342ada72b6919be8880c39bb Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 23 Dec 2021 15:56:01 +0100
Subject: [PATCH] add (?!) for nondependent contexts

---
 src/Quox/Context.idr      | 5 +++++
 src/Quox/Syntax/Shift.idr | 4 ++++
 2 files changed, 9 insertions(+)

diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index a7c00eb..54e38b2 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -75,6 +75,11 @@ public export %inline
 (!!) : CanShift tm => Context tm len -> Var len -> tm len
 ctx !! i = getShift ctx i SZ
 
+infixl 8 !?
+public export %inline
+(!?) : Context' tm len -> Var len -> tm
+ctx !? i = (ctx !! i) @{Const}
+
 
 ||| a triangle of bindings. each type binding in a context counts the ues of
 ||| others in its type, and all of these together form a triangle.
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index 5e23ebe..75b7b7e 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -204,3 +204,7 @@ interface CanShift f where
   (//) : f from -> Shift from to -> f to
 
 export CanShift Var where i // by = shift by i
+
+namespace CanShift
+  export
+  [Const] CanShift (\_ => a) where x // _ = x