From 18f17ad2b8d934e9dfec66752a951655bd09813a Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Mon, 30 Nov 2020 20:37:38 +0100
Subject: [PATCH] Moving code, importing equality

---
 paper/proof_irr.lp             | 1 +
 paper/stack.lp                 | 1 +
 {paper => sandbox}/rat_poly.lp | 0
 3 files changed, 2 insertions(+)
 rename {paper => sandbox}/rat_poly.lp (100%)

diff --git a/paper/proof_irr.lp b/paper/proof_irr.lp
index 6de8b6b..9563c73 100644
--- a/paper/proof_irr.lp
+++ b/paper/proof_irr.lp
@@ -1,6 +1,7 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.logical
+require open personoj.encodings.equality
 
 
 set declared "â„•"
diff --git a/paper/stack.lp b/paper/stack.lp
index 1561c41..04d1544 100644
--- a/paper/stack.lp
+++ b/paper/stack.lp
@@ -1,6 +1,7 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.logical
+require open personoj.encodings.equality
 
 constant symbol stack: Set
 constant symbol empty: El stack
diff --git a/paper/rat_poly.lp b/sandbox/rat_poly.lp
similarity index 100%
rename from paper/rat_poly.lp
rename to sandbox/rat_poly.lp
-- 
GitLab