From 90232dd1f82ff051e16e85f51f0552bf38d825ed Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 13 Mar 2023 19:32:52 +0100
Subject: [PATCH] rename some things to get rid of warnings

---
 lib/Quox/Pretty.idr             | 11 +++++------
 lib/Quox/Syntax/Dim.idr         |  2 +-
 lib/Quox/Syntax/Term/Pretty.idr | 14 +++++++-------
 lib/Quox/Syntax/Var.idr         |  2 +-
 4 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr
index 211d0c0..f2b3bc6 100644
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@@ -226,15 +226,14 @@ prettyTermDef : PrettyHL a => a -> IO Unit
 prettyTermDef = prettyTerm defPrettyOpts
 
 
-infixr 6 <//>
+infixr 6 <%%>, <%>
 export %inline
-(<//>) : Doc a -> Doc a -> Doc a
-a <//> b = sep [a, b]
+(<%%>) : Doc a -> Doc a -> Doc a
+a <%%> b = sep [a, b]
 
-infixr 6 </>
 export %inline
-(</>) : Doc a -> Doc a -> Doc a
-a </> b = cat [a, b]
+(<%>) : Doc a -> Doc a -> Doc a
+a <%> b = cat [a, b]
 
 
 
diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr
index 961e487..5145d0e 100644
--- a/lib/Quox/Syntax/Dim.idr
+++ b/lib/Quox/Syntax/Dim.idr
@@ -86,7 +86,7 @@ public export FromVar Dim where fromVar = B
 
 
 export
-inject : Dim d -> Dim (d + inj)
+inject : Dim d -> Dim (d + i)
 inject (K e) = K e
 inject (B i) = B $ inject i
 
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index d23c4a1..a6f5984 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -50,8 +50,8 @@ prettyBindType qtys x s arr t = do
   var <- prettyQtyBinds qtys $ TV x
   s   <- withPrec Outer $ prettyM s
   t   <- withPrec Outer $ under T x $ prettyM t
-  let bind = parens (var <++> colonD <//> hang 2 s)
-  parensIfM Outer $ hang 2 $ bind <//> t
+  let bind = parens (var <++> colonD <%%> hang 2 s)
+  parensIfM Outer $ hang 2 $ bind <%%> t
 
 export
 prettyArm : PrettyHL a => Pretty.HasEnv m =>
@@ -148,13 +148,13 @@ parameters (showSubsts : Bool)
     prettyM (CloT s th) =
       if showSubsts then
         parensIfM SApp . hang 2 =<<
-          [|withPrec SApp (prettyM s) </> prettyTSubst th|]
+          [|withPrec SApp (prettyM s) <%> prettyTSubst th|]
       else
         prettyM $ pushSubstsWith' id th s
     prettyM (DCloT s th) =
       if showSubsts then
         parensIfM SApp . hang 2 =<<
-          [|withPrec SApp (prettyM s) </> prettyDSubst th|]
+          [|withPrec SApp (prettyM s) <%> prettyDSubst th|]
       else
         prettyM $ pushSubstsWith' th id s
 
@@ -180,17 +180,17 @@ parameters (showSubsts : Bool)
     prettyM (s :# a) = do
       s <- withPrec AnnL $ prettyM s
       a <- withPrec Ann  $ prettyM a
-      parensIfM Ann $ hang 2 $ s <++> !annD <//> a
+      parensIfM Ann $ hang 2 $ s <++> !annD <%%> a
     prettyM (CloE e th)  =
       if showSubsts then
         parensIfM SApp . hang 2 =<<
-          [|withPrec SApp (prettyM e) </> prettyTSubst th|]
+          [|withPrec SApp (prettyM e) <%> prettyTSubst th|]
       else
         prettyM $ pushSubstsWith' id th e
     prettyM (DCloE e th) =
       if showSubsts then
         parensIfM SApp . hang 2 =<<
-          [|withPrec SApp (prettyM e) </> prettyDSubst th|]
+          [|withPrec SApp (prettyM e) <%> prettyDSubst th|]
       else
         prettyM $ pushSubstsWith' th id e
 
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index ef4197e..3102898 100644
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@@ -112,7 +112,7 @@ toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
 
 
 export
-inject : Var m -> Var (m + inj)
+inject : Var m -> Var (m + i)
 inject VZ     = VZ
 inject (VS i) = VS $ inject i