From ab828832145dc3a65eab666c97cda307d5bb81fa Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 25 Mar 2023 20:48:49 +0100
Subject: [PATCH] add weakD

---
 lib/Quox/Syntax/Dim.idr | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr
index 0f90b35..6d8ea7e 100644
--- a/lib/Quox/Syntax/Dim.idr
+++ b/lib/Quox/Syntax/Dim.idr
@@ -132,3 +132,8 @@ DecEq (Dim d) where
 public export %inline
 BV : (i : Nat) -> (0 _ : LT i d) => Dim d
 BV i = B $ V i
+
+
+export
+weakD : {default 1 by : Nat} -> Dim d -> Dim (by + d)
+weakD p = p // shift by