From e0bebc2557ed2e9ab72166d7acf1b6d6bee3ae31 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 15 Jul 2025 12:28:03 +0200
Subject: [PATCH] fix definitions of isLe and isGe

---
 Comp.lp | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Comp.lp b/Comp.lp
index ff334f3..2ceaa0e 100644
--- a/Comp.lp
+++ b/Comp.lp
@@ -38,15 +38,15 @@ with isGt Gt ↪ true;
 
 symbol isLe : Comp → 𝔹;
 
-rule isLt Eq ↪ true
-with isLt Lt ↪ true
-with isLt Gt ↪ false;
+rule isLe Eq ↪ true
+with isLe Lt ↪ true
+with isLe Gt ↪ false;
 
 symbol isGe : Comp → 𝔹;
 
-rule isLt Eq ↪ true
-with isLt Lt ↪ false
-with isLt Gt ↪ true;
+rule isGe Eq ↪ true
+with isGe Lt ↪ false
+with isGe Gt ↪ true;
 
 // Discriminate constructors