-
- Downloads
Code reorganization and helpers
Printer file moved to utilities New organisation of helpers, new helper file for RunningTheory and their elements. Can show Justifications SCProofCheckerJudgement now contain the proof they refer to, no need to pass it explicitely along anymore. Other small changes.
Showing
- src/main/scala/Example.scala 2 additions, 6 deletionssrc/main/scala/Example.scala
- src/main/scala/lisa/kernel/Printer.scala 0 additions, 333 deletionssrc/main/scala/lisa/kernel/Printer.scala
- src/main/scala/lisa/kernel/proof/Judgement.scala 4 additions, 3 deletionssrc/main/scala/lisa/kernel/proof/Judgement.scala
- src/main/scala/lisa/kernel/proof/RunningTheory.scala 46 additions, 25 deletionssrc/main/scala/lisa/kernel/proof/RunningTheory.scala
- src/main/scala/lisa/kernel/proof/SCProofChecker.scala 123 additions, 98 deletionssrc/main/scala/lisa/kernel/proof/SCProofChecker.scala
- src/main/scala/lisa/settheory/SetTheoryDefinitions.scala 1 addition, 1 deletionsrc/main/scala/lisa/settheory/SetTheoryDefinitions.scala
- src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala 2 additions, 1 deletionsrc/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
- src/main/scala/lisa/settheory/SetTheoryZAxioms.scala 1 addition, 1 deletionsrc/main/scala/lisa/settheory/SetTheoryZAxioms.scala
- src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala 1 addition, 1 deletionsrc/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
- src/main/scala/proven/DSetTheory/Part1.scala 7 additions, 15 deletionssrc/main/scala/proven/DSetTheory/Part1.scala
- src/main/scala/proven/ElementsOfSetTheory.scala 7 additions, 25 deletionssrc/main/scala/proven/ElementsOfSetTheory.scala
- src/main/scala/proven/tactics/Destructors.scala 1 addition, 1 deletionsrc/main/scala/proven/tactics/Destructors.scala
- src/main/scala/proven/tactics/ProofTactics.scala 2 additions, 2 deletionssrc/main/scala/proven/tactics/ProofTactics.scala
- src/main/scala/proven/tactics/SimplePropositionalSolver.scala 1 addition, 1 deletion...main/scala/proven/tactics/SimplePropositionalSolver.scala
- src/main/scala/utilities/KernelHelpers.scala 1 addition, 1 deletionsrc/main/scala/utilities/KernelHelpers.scala
- src/main/scala/utilities/TheoriesHelpers.scala 40 additions, 6 deletionssrc/main/scala/utilities/TheoriesHelpers.scala
- src/main/scala/utilities/tptp/KernelParser.scala 1 addition, 1 deletionsrc/main/scala/utilities/tptp/KernelParser.scala
- src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala 2 additions, 2 deletionssrc/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
- src/test/scala/lisa/kernel/FolTests.scala 2 additions, 2 deletionssrc/test/scala/lisa/kernel/FolTests.scala
- src/test/scala/lisa/kernel/IncorrectProofsTests.scala 1 addition, 1 deletionsrc/test/scala/lisa/kernel/IncorrectProofsTests.scala
Loading
Please register or sign in to comment