From: Anders Mörtberg <mortberg@chalmers.se>
Date: Mon, 20 Apr 2015 21:22:19 +0000 (+0200)
Subject: Fix printing of VPi
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=8e8143b7a9b07e2b85901743cf13048ae0873707;p=cubicaltt.git

Fix printing of VPi
---

diff --git a/CTT.hs b/CTT.hs
index 0d5bf49..b9dfb0b 100644
--- 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]