Skip to content
Snippets Groups Projects
Commit 5f70f712 authored by Katja Goltsova's avatar Katja Goltsova Committed by Viktor Kunčak
Browse files

Move all Peano-related files into their own package

parent 1b3106f4
No related branches found
No related tags found
3 merge requests!54Front integration,!53Front integration,!52Front integration
package lisa.proven.mathematics package lisa.proven.peano_example
import lisa.kernel.fol.FOL.* import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.SCProof import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.* import lisa.kernel.proof.SequentCalculus.*
import lisa.proven.PeanoArithmeticsLibrary
import lisa.proven.tactics.ProofTactics.* import lisa.proven.tactics.ProofTactics.*
import lisa.utils.Helpers.{_, given} import lisa.utils.Helpers.{_, given}
import lisa.utils.Library import lisa.utils.Library
import lisa.utils.Printer import lisa.utils.Printer
object Peano { object Peano {
export lisa.proven.PeanoArithmeticsLibrary.{*, given} export PeanoArithmeticsLibrary.{*, given}
/////////////////////////// OUTPUT CONTROL ////////////////////////// /////////////////////////// OUTPUT CONTROL //////////////////////////
given output: (String => Unit) = println given output: (String => Unit) = println
......
package lisa.proven.mathematics package lisa.proven.peano_example
import lisa.kernel.fol.FOL.* import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory import lisa.kernel.proof.RunningTheory
......
package lisa.proven package lisa.proven.peano_example
object PeanoArithmeticsLibrary extends lisa.utils.Library(lisa.proven.mathematics.PeanoArithmetics.runningPeanoTheory) { object PeanoArithmeticsLibrary extends lisa.utils.Library(lisa.proven.peano_example.PeanoArithmetics.runningPeanoTheory) {
export lisa.proven.mathematics.PeanoArithmetics.* export lisa.proven.peano_example.PeanoArithmetics.*
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment