@@ -50,7 +50,7 @@ mkApp tm [] = tm
5050mkApp tm (a::as) = mkApp (App tm a) as
5151
5252total
53−binderTy : (Eq t) => Binder t -> t
53+binderTy : Binder t -> t
5454binderTy (Lam t) = t
5555binderTy (Pi t _) = t
5656binderTy (Let t1 t2) = t1
@@ -75,7 +75,7 @@ mutual
7575 show (MetaN parent meta) = "(MetaN " ++ show parent ++ " " ++ show meta ++ ")"
7676
7777 instance Show TTName where
78− show (UN str) = "(UN " ++ str ++ ")"
78+ show (UN str) = "(UN " ++ show str ++ ")"
7979 show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
8080 show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"
8181 show (SN sn) = "(SN " ++ assert_total (show sn) ++ ")"
@@ -252,12 +252,12 @@ forget tm = fe [] tm
252252instance Show Raw where
253253 show r = my_show r
254254 where %assert_total my_show : Raw -> String
255− my_show (Var n) = "Var " ++ show n
256− my_show (RBind n b tm) = "RBind " ++ show n ++ " " ++ show b ++ " (" ++ my_show tm ++ ")"
257− my_show (RApp tm tm') = "RApp " ++ my_show tm ++ " " ++ my_show tm'
255+ my_show (Var n) = "(Var " ++ show n ++ ")"
256+ my_show (RBind n b tm) = "(RBind " ++ show n ++ " " ++ show b ++ " " ++ my_show tm ++ ")"
257+ my_show (RApp tm tm') = "(RApp " ++ my_show tm ++ " " ++ my_show tm' ++ ")"
258258 my_show RType = "RType"
259− my_show (RForce tm) = "RForce " ++ my_show tm
260− my_show (RConstant c) = "RConstant " ++ show c
259+ my_show (RForce tm) = "(RForce " ++ my_show tm ++ ")"
260+ my_show (RConstant c) = "(RConstant " ++ show c ++ ")"
261261
262262instance Show SourceLocation where
263263 show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col