Show for Name and Dim

lib/Quox/Name.idr

@@ -1,6 +1,7 @@
 module Quox.Name
 
 import public Data.SnocList
+import Data.List
 
 %default total
 
@@ -18,6 +19,11 @@ brepr (UN x) = x
 export Eq  BaseName where (==) = (==) `on` brepr
 export Ord BaseName where compare = compare `on` brepr
 
+export
+Show BaseName where
+  show (UN x) = x
+
+
 export
 baseStr : BaseName -> String
 baseStr (UN x) = x
@@ -42,6 +48,11 @@ repr x = (x.mods, brepr x.base)
 export Eq  Name where (==) = (==) `on` repr
 export Ord Name where compare = compare `on` repr
 
+export
+Show Name where
+  show (MakeName mods base) =
+    concat $ intersperse "." $ toList $ mods :< show base
+
 export
 FromString Name where
   fromString x = MakeName [<] (fromString x)

lib/Quox/Syntax/Dim.idr

@@ -37,6 +37,11 @@ drepr (B x) = Right x
 export Eq  (Dim n) where (==) = (==) `on` drepr
 export Ord (Dim n) where compare = compare `on` drepr
 
+export
+Show (Dim n) where
+  show (K k) = showCon App "K" $ show k
+  show (B i) = showCon App "B" $ show i
+
 export
 PrettyHL DimConst where
   prettyM Zero = hl Dim <$> ifUnicode "𝟬" "0"