From 5f70f71216340361336d95a9a52d7e5e547201fe Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Fri, 2 Sep 2022 15:49:22 +0200
Subject: [PATCH] Move all Peano-related files into their own package
---
src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala | 5 -----
.../lisa/proven/{mathematics => peano_example}/Peano.scala | 5 ++---
.../{mathematics => peano_example}/PeanoArithmetics.scala | 2 +-
.../lisa/proven/peano_example/PeanoArithmeticsLibrary.scala | 5 +++++
4 files changed, 8 insertions(+), 9 deletions(-)
delete mode 100644 src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala
rename src/main/scala/lisa/proven/{mathematics => peano_example}/Peano.scala (99%)
rename src/main/scala/lisa/proven/{mathematics => peano_example}/PeanoArithmetics.scala (98%)
create mode 100644 src/main/scala/lisa/proven/peano_example/PeanoArithmeticsLibrary.scala
diff --git a/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala b/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala
deleted file mode 100644
index 236926c7..00000000
--- a/src/main/scala/lisa/proven/PeanoArithmeticsLibrary.scala
+++ /dev/null
@@ -1,5 +0,0 @@
-package lisa.proven
-
-object PeanoArithmeticsLibrary extends lisa.utils.Library(lisa.proven.mathematics.PeanoArithmetics.runningPeanoTheory) {
- export lisa.proven.mathematics.PeanoArithmetics.*
-}
diff --git a/src/main/scala/lisa/proven/mathematics/Peano.scala b/src/main/scala/lisa/proven/peano_example/Peano.scala
similarity index 99%
rename from src/main/scala/lisa/proven/mathematics/Peano.scala
rename to src/main/scala/lisa/proven/peano_example/Peano.scala
index 78b3244e..ca74d815 100644
--- a/src/main/scala/lisa/proven/mathematics/Peano.scala
+++ b/src/main/scala/lisa/proven/peano_example/Peano.scala
@@ -1,17 +1,16 @@
-package lisa.proven.mathematics
+package lisa.proven.peano_example
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
-import lisa.proven.PeanoArithmeticsLibrary
import lisa.proven.tactics.ProofTactics.*
import lisa.utils.Helpers.{_, given}
import lisa.utils.Library
import lisa.utils.Printer
object Peano {
- export lisa.proven.PeanoArithmeticsLibrary.{*, given}
+ export PeanoArithmeticsLibrary.{*, given}
/////////////////////////// OUTPUT CONTROL //////////////////////////
given output: (String => Unit) = println
diff --git a/src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala b/src/main/scala/lisa/proven/peano_example/PeanoArithmetics.scala
similarity index 98%
rename from src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala
rename to src/main/scala/lisa/proven/peano_example/PeanoArithmetics.scala
index 62801b59..03797ff2 100644
--- a/src/main/scala/lisa/proven/mathematics/PeanoArithmetics.scala
+++ b/src/main/scala/lisa/proven/peano_example/PeanoArithmetics.scala
@@ -1,4 +1,4 @@
-package lisa.proven.mathematics
+package lisa.proven.peano_example
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
diff --git a/src/main/scala/lisa/proven/peano_example/PeanoArithmeticsLibrary.scala b/src/main/scala/lisa/proven/peano_example/PeanoArithmeticsLibrary.scala
new file mode 100644
index 00000000..ca4c98bf
--- /dev/null
+++ b/src/main/scala/lisa/proven/peano_example/PeanoArithmeticsLibrary.scala
@@ -0,0 +1,5 @@
+package lisa.proven.peano_example
+
+object PeanoArithmeticsLibrary extends lisa.utils.Library(lisa.proven.peano_example.PeanoArithmetics.runningPeanoTheory) {
+ export lisa.proven.peano_example.PeanoArithmetics.*
+}
--
GitLab