From 1aece6a70777cdea493c9afc10d728c90449c81e Mon Sep 17 00:00:00 2001
From: Aleksander Wolska <odderwiser@gmail.com>
Date: Tue, 7 May 2024 17:46:40 +0200
Subject: [PATCH] test fix
---
test/LawfulOrd.agda | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/test/LawfulOrd.agda b/test/LawfulOrd.agda
index 6027f6ab..5fdb054f 100644
--- a/test/LawfulOrd.agda
+++ b/test/LawfulOrd.agda
@@ -13,7 +13,7 @@ nLtEq2Gt : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
nLtEq2Gt x y ⦃ h1 ⦄ ⦃ h2 ⦄ =
begin
(x > y)
- ≡⟨ sym (not-involution (x <= y) (x > y) (lte2ngt x y)) ⟩
+ ≡⟨ sym (not-involution (lte2ngt x y)) ⟩
not (x <= y)
≡⟨ cong not (lte2LtEq x y) ⟩
not ((x < y) || (x == y))