Merge pull request #65 from cache-nez/and-or-one-argument

Print and/or connector formulas with 1 argument

lisa-utils/src/main/scala/lisa/utils/Parser.scala

@@ -460,6 +460,7 @@ object Parser {
       },
       {
         case ConnectorFormula(c @ (Iff | Implies), Seq(left, right)) => Seq(left ~ Some(c ~ right))
+        case ConnectorFormula((And | Or), Seq(f)) => Seq(f ~ None)
         case f => Seq(f ~ None)
       }
     )

lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala

@@ -98,6 +98,15 @@ class PrinterTest extends AnyFunSuite with TestUtils {
     assert(Parser.printFormula(ConnectorFormula(Or, Seq(ConnectorFormula(Or, Seq(a, b)), c))) == "a ∨ b ∨ c")
   }
 
+  test("and/or of 1 argument") {
+    assert(Parser.printFormula(ConnectorFormula(And, Seq(a))) == "a")
+    assert(Parser.printFormula(ConnectorFormula(Or, Seq(a))) == "a")
+
+    assert(Parser.printFormula(ConnectorFormula(Implies, Seq(ConnectorFormula(Or, Seq(a)), ConnectorFormula(And, Seq(a))))) == "(a) ⇒ (a)")
+    assert(Parser.printFormula(ConnectorFormula(Implies, Seq(a, a))) == "a ⇒ a")
+    assert(Parser.printFormula(BinderFormula(Forall, x, ConnectorFormula(Or, Seq(a)))) == "∀'x. a")
+  }
+
   test("connectors of >2 arguments") {
     assert(Parser.printFormula(ConnectorFormula(And, Seq(a, b, c))) == "a ∧ b ∧ c")
     assert(Parser.printFormula(ConnectorFormula(Or, Seq(a, b, c))) == "a ∨ b ∨ c")