Fix printing of VPi

diff --git a/CTT.hs b/CTT.hs
index 0d5bf49ebeb496be7746d39cb6e4f8a6ba107c1c..b9dfb0b304073cdecfc31efe9196bf05272dd2ed 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -380,9 +380,9 @@ showVal v = case v of
   VCon c us         -> text c <+> showVals us
   VPCon c a us phis -> text c <+> braces (showVal a) <+> showVals us
                        <+> (hsep $ map ((char '@' <+>) . showFormula) phis)
-  VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->"
-                                               <+> showVal1 b
-                       | otherwise -> showVal l
+  VPi a l@(VLam x t b)
+    | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b
+    | otherwise -> parens (text x <+> colon <+> showVal t) <+> text "->" <+> showVal b
   VPi a b           -> text "Pi" <+> showVals [a,b]
   VPair u v         -> parens (showVal u <> comma <> showVal v)
   VSigma u v        -> text "Sigma" <+> showVals [u,v]