left side of meta identity can be anything

README.md

@@ -22,7 +22,7 @@ constantly being updated to follow more recent developments.
 ## Install
 [![Maven Central](https://img.shields.io/maven-central/v/io.github.leoprover/scala-tptp-parser_2.13.svg?label=Maven%20Central)](https://search.maven.org/search?q=g:%22io.github.leoprover%22%20AND%20a:%22scala-tptp-parser_2.13%22)
 
-The Scala TPTP parser is available on [Maven Central](https://search.maven.org/artifact/io.github.leoprover/scala-tptp-parser_2.13) (current version: 1.7.0).
+The Scala TPTP parser is available on [Maven Central](https://search.maven.org/artifact/io.github.leoprover/scala-tptp-parser_2.13) (current version: 1.7.1).
 Snapshots are available on [Sonatype](https://s01.oss.sonatype.org/content/repositories/snapshots/io/github/leoprover/scala-tptp-parser_2.13/).
 
 ### Maven
@@ -32,15 +32,15 @@ In order to include `scala-tptp-parser` into your project via Maven, just add th
 <dependency>
   <groupId>io.github.leoprover</groupId>
   <artifactId>scala-tptp-parser_2.13</artifactId>
-  <version>1.7.0</version>
+  <version>1.7.1</version>
 </dependency>
 ```
 
 ### sbt
 
 In order to include `scala-tptp-parser` into your project via SBT, just add the following dependency to your `build.sbt`:
 ```scala
-libraryDependencies += "io.github.leoprover" %% "scala-tptp-parser" % "1.7.0"
+libraryDependencies += "io.github.leoprover" %% "scala-tptp-parser" % "1.7.1"
 ```
 
 ### Non-sbt-projects
@@ -92,6 +92,7 @@ try {
 
 ## Version history
 
+  - 1.7.1: Allow any TFF terms on the left side of a meta equality (==).
   - 1.7.0: Rework non-classical formulas in TFF and THF, so that both languages now have their dedicated case class for non-classical formulas, called `NonclassicalPolyaryFormula`. This breaks a few things from previous versions (new formula structure for NCL formulas).
            Also, the NCL short-form connectives `[.]` and `<.>` are now unary connectives (and can be used as such). The long-form connectives `{name}` still require an explicit application with `@`.
   - 1.6.5: Fix usage of single-quoted identifiers that start with $ (or $$). Now the single quotes are retained in the functor name (in the AST) if the name is not a TPTP lower word. So the functor with name (as string) "$true" is not equal to "'$true'", as it should be (note the single quotes in the second variant). Single quotes are stripped automatically, if they are not necessary (i.e., parsing "'abc'" will produce functor "abc" without single quotes). 

src/main/scala/leo/datastructures/TPTP.scala

@@ -761,11 +761,11 @@ object TPTP {
       }
       override def symbols: Set[String] = typing.keySet ++ body.symbols
     }
-    final case class Assignment(lhs: AtomicTerm, rhs: Term) extends Formula {
+    final case class Assignment(lhs: Term, rhs: Term) extends Formula {
       override def pretty: String = s"(${lhs.pretty}) := (${rhs.pretty})"
       override def symbols: Set[String] = lhs.symbols ++ rhs.symbols
     }
-    final case class MetaIdentity(lhs: AtomicTerm, rhs: Term) extends Formula {
+    final case class MetaIdentity(lhs: Term, rhs: Term) extends Formula {
       override def pretty: String = s"(${lhs.pretty}) == (${rhs.pretty})"
       override def symbols: Set[String] = lhs.symbols ++ rhs.symbols
     }

src/main/scala/leo/modules/input/TPTPParser.scala

@@ -1562,11 +1562,12 @@ object TPTPParser {
       // To allow := bindings with arbitrary formulas (w/o parentheses), i.e., have := a very low binding strength
       val f1 = tffLogicFormula0(tfx)
       if (tfx && o(IDENTITY, null) != null) { // Only allow '==' in TFX mode
+        val f2 = tffLogicFormulaOrTerm0() // Terms are more general, since they can also be formulas in TFX
         f1 match {
           case TFF.AtomicFormula(f, args) =>
-            val f2 = tffLogicFormulaOrTerm0() // Terms are more general, since they can also be formulas in TFX
             TFF.MetaIdentity(TFF.AtomicTerm(f, args), f2)
-          case _ => error2(s"Parse error: Unexpected left-hand side of assignmeht '${f1.pretty}'. Only atomic terms are permitted.", lastTok)
+          case TFF.FormulaVariable(name) => TFF.MetaIdentity(TFF.Variable(name), f2)
+          case _ => TFF.MetaIdentity(TFF.FormulaTerm(f1), f2)
         }
       } else f1
     }
@@ -1993,12 +1994,8 @@ object TPTPParser {
       // To allow '==' bindings with arbitrary formulas or terms (w/o parentheses), i.e., have '==' a very low binding strength
       val f1 = tffLogicFormulaOrTerm0()
       if (o(IDENTITY, null) != null) {
-        f1 match {
-          case at@TFF.AtomicTerm(_, _) =>
-            val f2 = tffLogicFormulaOrTerm0()
-            TFF.FormulaTerm(TFF.MetaIdentity(at, f2))
-          case _ => error2(s"Parse error: Unexpected left-hand side of assignmeht '${f1.pretty}'. Only atomic terms are permitted.", lastTok)
-        }
+        val f2 = tffLogicFormulaOrTerm0()
+        TFF.FormulaTerm(TFF.MetaIdentity(f1, f2))
       } else f1
     }