From 9bd02d185a24c1949bbc43c1f94e2986138f9f20 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 27 Feb 2022 01:28:36 +0100
Subject: [PATCH] add Context.pure

---
 src/Quox/Context.idr | 42 ++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 40 insertions(+), 2 deletions(-)

diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index 6a22835..123cb18 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -149,8 +149,46 @@ export %inline
 (<*>) : Telescope (\n => tm1 n -> tm2 n) from to ->
         Telescope tm1 from to -> Telescope tm2 from to
 ftel <*> xtel = runIdentity $ (pure .) <$> ftel `app` xtel
--- ...but can't write pure without `from,to` being relevant,
--- so no idiom brackets ☹
+-- ...but can't write pure without `from,to` being ω, so no idiom brackets ☹
+
+
+namespace Nat
+  public export
+  data LTE' : Nat -> Nat -> Type where
+    LTERefl  : n `LTE'` n
+    LTESuccR : m `LTE'` n -> m `LTE'` S n
+  %builtin Natural LTE'
+
+  export
+  lteZero' : {n : Nat} -> 0 `LTE'` n
+  lteZero' {n = 0}   = LTERefl
+  lteZero' {n = S n} = LTESuccR lteZero'
+
+  export
+  lteSucc' : m `LTE'` n -> S m `LTE'` S n
+  lteSucc' LTERefl      = LTERefl
+  lteSucc' (LTESuccR p) = LTESuccR (lteSucc' p)
+
+  export
+  lteToLte' : {n : Nat} -> m `LTE` n -> m `LTE'` n
+  lteToLte' LTEZero     = lteZero'
+  lteToLte' (LTESucc p) = lteSucc' (lteToLte' p)
+
+  export
+  lte'ToLte : {n : Nat} -> m `LTE'` n -> m `LTE` n
+  lte'ToLte LTERefl      = reflexive {rel=Nat.LTE}
+  lte'ToLte (LTESuccR p) = lteSuccRight (lte'ToLte p)
+
+  export
+  teleLte' : Telescope tm from to -> from `LTE'` to
+  teleLte' [<]        = LTERefl
+  teleLte' (tel :< _) = LTESuccR (teleLte' tel)
+
+
+export
+pure : from `LTE'` to => a -> Telescope' a from to
+pure @{LTERefl}    x = [<]
+pure @{LTESuccR _} x = pure x :< x
 
 
 export %inline