From 13b173322ba2ca03ad726f14d6c544bd82da6153 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 9 Apr 2022 18:55:08 +0200
Subject: [PATCH] %inline, etc

---
 src/Quox/Pretty.idr | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/Quox/Pretty.idr b/src/Quox/Pretty.idr
index d6178ef..f597f1d 100644
--- a/src/Quox/Pretty.idr
+++ b/src/Quox/Pretty.idr
@@ -40,8 +40,8 @@ hlRepr Qty     = 6
 hlRepr Free    = 7
 hlRepr Syntax  = 8
 
-export Eq  HL where (==) = (==) `on` hlRepr
-export Ord HL where compare = compare `on` hlRepr
+export %inline Eq  HL where (==) = (==) `on` hlRepr
+export %inline Ord HL where compare = compare `on` hlRepr
 
 
 public export
@@ -52,7 +52,7 @@ data PPrec
   -- ...
   | App  -- term/dimension application
   | SApp -- substitution application
-  | Arg
+  | Arg  -- argument to nonfix function
 
 private PrecRepr : Type
 PrecRepr = Nat
@@ -66,8 +66,8 @@ precRepr App   = 98
 precRepr SApp  = 99
 precRepr Arg   = 100
 
-export Eq  PPrec where (==) = (==) `on` precRepr
-export Ord PPrec where compare = compare `on` precRepr
+export %inline Eq  PPrec where (==) = (==) `on` precRepr
+export %inline Ord PPrec where compare = compare `on` precRepr
 
 
 export %inline
@@ -128,7 +128,7 @@ record PrettyEnv where
   ||| surrounding precedence level
   prec    : PPrec
 
-public export %inline HasEnv : (Type -> Type) -> Type
+public export HasEnv : (Type -> Type) -> Type
 HasEnv = MonadReader PrettyEnv
 
 export %inline
@@ -147,9 +147,8 @@ public export data BinderSort = T | D
 
 export %inline
 under : HasEnv m => BinderSort -> Name -> m a -> m a
-under s x = local $
-  {prec := Outer} .
-  (case s of T => {tnames $= (x ::)}; D => {dnames $= (x ::)})
+under T x = local {prec := Outer, tnames $= (x ::)}
+under D x = local {prec := Outer, dnames $= (x ::)}
 
 
 public export