@@ -264,6 +264,18 @@ implementation Eq TT where
264264 equalp (UType u) (UType u') = u == u'
265265 equalp x y = False
266266
267+implementation Eq Raw where
268+ a == b = equalp a b
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
276+ equalp _ _ = False
277+
278+
267279total
268280forget : TT -> Maybe Raw
269281forget tm = fe [] tm