From 76c02adf0370670697a0a3cca049f5adab504af7 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 27 Feb 2022 01:46:44 +0100
Subject: [PATCH] add Subst.one

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

diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index 6035633..1c5451c 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -90,6 +90,11 @@ drop1 (Shift by) = Shift $ drop1 by
 drop1 (t ::: th) = th
 
 
+public export %inline
+one : f n -> Subst f (S n) n
+one x = x ::: id
+
+
 ||| `prettySubst pr names bnd op cl th` pretty-prints the substitution `th`,
 ||| with the following arguments:
 |||