e81efdb · Idris-dev · git.iko.soy

50mkApp tm (a::as) = mkApp (App tm a) as

51

52total

53−binderTy : (Eq t) => Binder t -> t

53+binderTy : Binder t -> t

54binderTy (Lam t) = t

55binderTy (Pi t _) = t

56binderTy (Let t1 t2) = t1

75 show (MetaN parent meta) = "(MetaN " ++ show parent ++ " " ++ show meta ++ ")"

76

77 instance Show TTName where

78− show (UN str) = "(UN " ++ str ++ ")"

78+ show (UN str) = "(UN " ++ show str ++ ")"

79 show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"

80 show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"

81 show (SN sn) = "(SN " ++ assert_total (show sn) ++ ")"

252instance Show Raw where

253 show r = my_show r

254 where %assert_total my_show : Raw -> String

255− my_show (Var n) = "Var " ++ show n

255+ my_show (Var n) = "(Var " ++ show n ++ ")"

256− my_show (RBind n b tm) = "RBind " ++ show n ++ " " ++ show b ++ " (" ++ my_show tm ++ ")"

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'

257+ my_show (RApp tm tm') = "(RApp " ++ my_show tm ++ " " ++ my_show tm' ++ ")"

258 my_show RType = "RType"

259− my_show (RForce tm) = "RForce " ++ my_show tm

259+ my_show (RForce tm) = "(RForce " ++ my_show tm ++ ")"

260− my_show (RConstant c) = "RConstant " ++ show c

260+ my_show (RConstant c) = "(RConstant " ++ show c ++ ")"

261

262instance Show SourceLocation where

263 show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col