From: Anders Mörtberg <mortberg@chalmers.se>
Date: Fri, 17 Apr 2015 08:50:01 +0000 (+0200)
Subject: Only show second part of VPi x (VLam ...)
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=c2ddee06257a13823a6a3abcecb87d30473b6e79;p=cubicaltt.git

Only show second part of VPi x (VLam ...)
---

diff --git a/CTT.hs b/CTT.hs
index 4f40cd6..7b20d3a 100644
--- a/CTT.hs
+++ b/CTT.hs
@@ -367,7 +367,8 @@ showVal v = case v of
   VCon c us         -> text c <+> showVals us
   VPCon c a us phi  -> text c <+> char '{' <+> showVal a <+> char '}' <+>
                        showVals us <+> showFormula phi
-  VPi a (VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b
+  VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b
+                       | otherwise -> showVal l
   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]