From ba77c45c644d4653e064daf9408a17141e2ae34c Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 26 Aug 2023 21:19:40 +0200
Subject: [PATCH] always print the direction in coe/comp

---
 lib/Quox/Syntax/Term/Pretty.idr | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 3b91f49..ab40679 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -524,17 +524,12 @@ prettyElim dnames tnames (Ann tm ty _) =
                 !(withPrec Outer (prettyTerm dnames tnames ty))
 
 prettyElim dnames tnames (Coe ty p q val _) =
-  parensIfM App =<<
-    if isDefaultDir p q then do
-      ty  <- prettyTypeLine dnames tnames ty
-      val <- prettyTArg dnames tnames val
-      prettyAppD !coeD [ty, val]
-    else do
-      ty  <- prettyTypeLine dnames tnames ty
-      p   <- prettyDArg dnames p
-      q   <- prettyDArg dnames q
-      val <- prettyTArg dnames tnames val
-      prettyAppD !coeD [ty, sep [p, q], val]
+  parensIfM App =<< do
+    ty  <- prettyTypeLine dnames tnames ty
+    p   <- prettyDArg dnames p
+    q   <- prettyDArg dnames q
+    val <- prettyTArg dnames tnames val
+    prettyAppD !coeD [ty, sep [p, q], val]
 
 prettyElim dnames tnames e@(Comp ty p q val r zero one _) =
   parensIfM App =<< do
@@ -545,9 +540,7 @@ prettyElim dnames tnames e@(Comp ty p q val r zero one _) =
     arm0 <- [|prettyCompArm dnames tnames Zero zero <+> semiD|]
     arm1 <- prettyCompArm dnames tnames One one
     ind  <- askAt INDENT
-    if isDefaultDir p q
-       then layoutComp [ty]     val r [arm0, arm1]
-       else layoutComp [ty, pq] val r [arm0, arm1]
+    layoutComp [ty, pq] val r [arm0, arm1]
 
 prettyElim dnames tnames (TypeCase ty ret arms def _) = do
   arms <- for (toList arms) $ \(k ** body) => do