diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index 6bde70a..91dcde5 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -139,7 +139,11 @@ tests = "equality & subtyping" :- [ (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 0), testEq "λ x ⇒ [a] ≡ λ x ⇒ [a] (TUsed vs TUnused)" $ equalT (Lam "x" $ TUsed $ FT "a") - (Lam "x" $ TUnused $ FT "a") + (Lam "x" $ TUnused $ FT "a"), + skipWith "(no η yet)" $ + testEq "λ x ⇒ [f [x]] ≡ [f] (η)" $ + equalT (Lam "x" $ TUsed $ E $ F "f" :@ BVT 0) + (FT "f") ], "term closure" :- [