@@ -264,6 +264,18 @@ implementation Eq TT where
264 equalp (UType u) (UType u') = u == u'
264 equalp (UType u) (UType u') = u == u'
265 equalp x y = False
265 equalp x y = False
267+implementation Eq Raw where
269+ where equalp : Raw -> Raw -> Bool
270+ equalp (Var x) (Var y) = x == y
271+ equalp (RBind x b1 e1) (RBind y b2 e2) = x == y && b1 == b2 && e1 == e2
272+ equalp (RApp f1 a1) (RApp f2 a2) = f1 == f2 && a1 == a2
273+ equalp RType RType = True
274+ equalp (RUType u1) (RUType u2) = u1 == u2
275+ equalp (RConstant c1) (RConstant c2) = c1 == c2
268forget : TT -> Maybe Raw
280forget : TT -> Maybe Raw
269forget tm = fe [] tm
281forget tm = fe [] tm