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

diff --git a/CTT.hs b/CTT.hs
index 4f40cd6f25e65bb0f37948b5301b2f9a3c7ed6e4..7b20d3aa7345c79d88e6015962231b46b5265070 100644 (file)
--- 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]