From 8fae67d4d56ab94a673ab724d1056243b5e145f2 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 12 May 2024 20:32:32 +0200
Subject: [PATCH] check the new test actually fails in the right way

---
 golden-tests/tests/eta-singleton/eta-sing.quox | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/golden-tests/tests/eta-singleton/eta-sing.quox b/golden-tests/tests/eta-singleton/eta-sing.quox
index c3b1fc3..5ae2daf 100644
--- a/golden-tests/tests/eta-singleton/eta-sing.quox
+++ b/golden-tests/tests/eta-singleton/eta-sing.quox
@@ -27,7 +27,7 @@ namespace unrestricted {
 namespace linear {
   def0 ZZA : ★ = 1.ZZ → A
 
-  #[fail]
+  #[fail "λ _ ⇒ x reflZ is not equal to x"]
   def defeq : 0.(P : ZZA → ★) → 0.(x : ZZA) → P (λ _ ⇒ x reflZ) → P x =
     λ P x p ⇒ p
 }