From 961c8415b52aa13f3b74e38a3a5c0578c8dd7ae4 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 8 Jan 2023 15:44:29 +0100
Subject: [PATCH] =?UTF-8?q?a=20skipped=20=CE=B7=20test?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 tests/Tests/Equal.idr | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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" :- [