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