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