@@ -110,7 +110,7 @@ data TT n = P NameType n (TT n) -- embed type
110110 | Bind n (Binder (TT n)) (TT n)
111111 | App (TT n) (TT n) -- function, function type, arg
112112 | Set Int
113− deriving (Functor, Eq)
113+ deriving Functor
114114
115115type EnvTT n = [(n, Binder (TT n))]
116116
@@ -119,6 +119,14 @@ data Datatype n = Data { d_typename :: n,
119119 d_cons :: [(n, TT n)] }
120120 deriving (Show, Functor, Eq)
121121
122+instance Eq n => Eq (TT n) where
123+ (==) (P xt x _) (P yt y _) = xt == yt && x == y
124+ (==) (V x) (V y) = x == y
125+ (==) (Bind _ xb xs) (Bind _ yb ys) = xb == yb && xs == ys
126+ (==) (App fx ax) (App fy ay) = fx == fy && ax == ay
127+ (==) (Set x) (Set y) = x == y
128+ (==) _ _ = False
129+
122130-- A few handy operations on well typed terms:
123131
124132-- Returns true if V 0 and bound name n do not occur in the term
@@ -177,12 +185,12 @@ showEnvDbg env t = showEnv' env t True
177185
178186showEnv' env t dbg = se 10 env t where
179187 se p env (P nt n t) = show n
180−-- ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
188+ ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
181189 se p env (V i) | i < length env = (show $ fst $ env!!i) ++
182190 if dbg then "{" ++ show i ++ "}" else ""
183191 | otherwise = "!!V " ++ show i ++ "!!"
184− se p env (Bind n b@(Pi t) sc)
185− | noOccurrence n sc = bracket p 2 $ se 10 env t ++ " -> " ++ se 10 ((n,b):env) sc
192+ se p env (Bind n b@(Pi t) sc)
193+ | noOccurrence n sc && not dbg = bracket p 2 $ se 10 env t ++ " -> " ++ se 10 ((n,b):env) sc
186194 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc
187195 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
188196 se p env (Set i) = "Set" ++ show i