Skip to content
Snippets Groups Projects
Commit 6a25924b authored by SimonGuilloud's avatar SimonGuilloud
Browse files

trying to sastisfy the CI 5.

parent 4f97ea70
No related branches found
No related tags found
6 merge requests!62Easy tactics,!58Easy tactics,!55Front integration and various changes,!54Front integration,!53Front integration,!52Front integration
This commit is part of merge request !53. Comments created here will be created in the context of that merge request.
package lisa.front
import lisa.front.{_, given}
import lisa.front.{*, given}
import org.scalatest.funsuite.AnyFunSuite
import scala.language.adhocExtensions
......
......@@ -4,7 +4,7 @@ import lisa.front.fol.FOL.LabelType
import lisa.front.fol.FOL.WithArityType
import lisa.front.printer.FrontPositionedPrinter
import lisa.front.printer.FrontPrintStyle
import lisa.front.{_, given}
import lisa.front.{*, given}
import org.scalatest.Ignore
import org.scalatest.funsuite.AnyFunSuite
......
......@@ -6,7 +6,7 @@ import lisa.kernel.proof.RunningTheory.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SequentCalculus.*
import lisa.utils.Helpers.{_, given}
import lisa.utils.Helpers.{*, given}
import lisa.utils.Printer
import org.scalatest.funsuite.AnyFunSuite
......
......@@ -4,7 +4,7 @@ import lisa.kernel.proof.SCProofCheckerJudgement.SCInvalidProof
import lisa.kernel.proof.SequentCalculus.*
import lisa.kernel.proof.*
import lisa.test.ProofCheckerSuite
import lisa.utils.Helpers.{_, given}
import lisa.utils.Helpers.{*, given}
class InvalidProofPathTests extends ProofCheckerSuite {
def checkPath(invalidProof: SCProof, expectedPath: Seq[Int]): Unit = {
......
......@@ -6,7 +6,7 @@ import lisa.kernel.proof.RunningTheory.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SequentCalculus.*
import lisa.utils.Helpers.{_, given}
import lisa.utils.Helpers.{*, given}
import lisa.utils.Printer
import org.scalatest.funsuite.AnyFunSuite
......
......@@ -6,7 +6,7 @@ import lisa.kernel.proof.SCProofCheckerJudgement
import lisa.kernel.proof.SCProofCheckerJudgement.SCInvalidProof
import lisa.kernel.proof.SequentCalculus.Sequent
import lisa.kernel.proof.SequentCalculus.isSameSequent
import lisa.utils.Helpers.{_, given}
import lisa.utils.Helpers.{*, given}
import lisa.utils.Printer
import org.scalatest.funsuite.AnyFunSuite
......
......@@ -2,7 +2,7 @@ package lisa.test
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.utils.Helpers.{_, given}
import lisa.utils.Helpers.{*, given}
trait TestTheoryAxioms {
final val p1 = ConstantPredicateLabel("p1", 1)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment