diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..29325cc --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "lisa"] + path = lisa + url = git@github.com:epfl-lara/lisa.git diff --git a/build.sbt b/build.sbt new file mode 100644 index 0000000..b16781e --- /dev/null +++ b/build.sbt @@ -0,0 +1,8 @@ +name := "master-project" + +version := "0.1" + +scalaVersion := "2.13.8" + +lazy val lisa = RootProject(file("lisa")) +lazy val root = (project in file(".")).dependsOn(lisa) diff --git a/lisa b/lisa new file mode 160000 index 0000000..9a3a4a5 --- /dev/null +++ b/lisa @@ -0,0 +1 @@ +Subproject commit 9a3a4a59c1291f487d0b5789792e6c94aa32ef49 diff --git a/project/build.properties b/project/build.properties new file mode 100644 index 0000000..b46cfa1 --- /dev/null +++ b/project/build.properties @@ -0,0 +1 @@ +sbt.version = 1.6.2 \ No newline at end of file diff --git a/src/main/scala/Main.scala b/src/main/scala/Main.scala new file mode 100644 index 0000000..7bfb891 --- /dev/null +++ b/src/main/scala/Main.scala @@ -0,0 +1,12 @@ +import lisa.kernel.Printer +import lisa.kernel.fol.FOL._ +import lisa.KernelHelpers._ + +object Main extends App { + + val (la, lb) = (ConstantPredicateLabel("a", 0), ConstantPredicateLabel("b", 0)) + val (a, b) = (PredicateFormula(la, Seq.empty), PredicateFormula(lb, Seq.empty)) + + println(Printer.prettyFormula((a \/ b) /\ a)) + +}