From a186c15477283242192bde8bd9df59030f7e2cf5 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 13 Nov 2024 22:03:00 -0800 Subject: [PATCH] suppress closure env in printing --- newt/Combinatory.newt | 2 +- src/Lib/Types.idr | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/newt/Combinatory.newt b/newt/Combinatory.newt index d05e96d..09dfa9c 100644 --- a/newt/Combinatory.newt +++ b/newt/Combinatory.newt @@ -78,7 +78,7 @@ sapp (CApp K t) (CApp K u) = CApp K (CApp t u) -- was out of pattern because of unexpanded lets. sapp (CApp K t) u = CApp (CApp B t) u -- TODO unsolved meta, out of pattern fragment -sapp t (CApp K u) = ? -- CApp (CApp C t) u +sapp t (CApp K u) = CApp (CApp C t) u -- TODO unsolved meta, out of pattern fragment sapp t u = ? -- CApp (CApp S t) u diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index ffc9d45..c3d6bad 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -266,7 +266,7 @@ Show Val where show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> [])})" show (VRef _ nm _ [<]) = nm show (VRef _ nm _ sp) = "(\{nm} \{unwords $ map show (sp <>> [])})" - show (VMeta _ ix sp) = "(%meta \{show ix} ..\{show $ length sp})" + show (VMeta _ ix sp) = "(%meta \{show ix} [\{show $ length sp} sp])" show (VLam _ str x) = "(%lam \{str} \{show x})" show (VPi fc str Implicit x y) = "(%pi {\{str} : \{show x}}. \{show y})" show (VPi fc str Explicit x y) = "(%pi (\{str} : \{show x}). \{show y})" @@ -299,7 +299,7 @@ data Closure = MkClosure Env Tm covering Show Closure where - show (MkClosure xs t) = "(%cl \{show xs} \{show t})" + show (MkClosure xs t) = "(%cl [\{show $ length xs} env] \{show t})" {- smalltt