From 8e9b0abb34bf21fd7272e67fef2ed2669322c372 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 13 Mar 2023 18:25:07 +0100
Subject: [PATCH] Show Telescope

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

diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index a2cd868..9ffe7da 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -221,6 +221,11 @@ export %inline
 (forall n. Ord (tm n)) => Ord (Telescope tm from to) where
   compare = foldLazy .: zipWithLazy compare
 
+export %inline
+(forall n. Show (tm n)) => Show (Telescope tm from to) where
+  showPrec d = showPrec d . toSnocList
+    where Show (Exists tm) where showPrec d t = showPrec d t.snd
+
 export %inline
 (forall n. PrettyHL (tm n)) => PrettyHL (Telescope tm from to) where
   prettyM tel = separate (hl Delim ";") <$> traverse prettyM (toList tel)