From 91189d33330ceffa62fa5aea7004dc3e1805dc7b Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Wed, 5 Oct 2022 12:59:09 +0200
Subject: [PATCH] Define ordered pair with name 'pair' instead of the empty one
---
src/main/scala/lisa/proven/mathematics/SetTheory.scala | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/main/scala/lisa/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
index d677546e..611c82a5 100644
--- a/src/main/scala/lisa/proven/mathematics/SetTheory.scala
+++ b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
@@ -359,7 +359,7 @@ object SetTheory extends lisa.Main {
private val x = VariableLabel("x")
private val y = VariableLabel("y")
- val oPair: ConstantFunctionLabel = DEFINE("", x, y) as pair(pair(x, y), pair(x, x))
+ val oPair: ConstantFunctionLabel = DEFINE("pair", x, y) as unorderedPair(unorderedPair(x, y), unorderedPair(x, x))
show
}
--
GitLab