From c2ddee06257a13823a6a3abcecb87d30473b6e79 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <mortberg@chalmers.se>
Date: Fri, 17 Apr 2015 10:50:01 +0200
Subject: [PATCH] Only show second part of VPi x (VLam ...)

---
 CTT.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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]
-- 
2.34.1