* Simplify parsing of predicate application

* Change lexing of identifiers:

* schematic symbols can only be variable-like: a mix of letters, digits, and _, preceded by '
* constant symbols can be:
  - variable-like
  - sequence of digits
  - sequence of selected ASCII characters to allow ids such as ++, ::
  - 1 arbitrary non-whitespace symbol
* constant symbols can be path-qualified (a path is words, separated by $: abc$def$): algebra$matrices$*
  Since paths are currently not supported by LISA, the path gets merged into the id on the lexer level.
  This is a temporary behaviour to be changed once paths are supported.

* Generalize supported infix predicates

In addition to equality, parse as infix all predicates on whose names isInfix
returns true

* Simple tactic for substitution of equals for equals and equivalent for equivalents.
* Some corrections in the EquivalenceChecker
* Moved InstantiateBinder to helpers.
* Some more changes regarding tactics and proof steps.

* Correct bug related to instantiatePredicateSchemas not instantiating variable formulas

* Corrected bug linked to the equivalence checker no distinguishing schematic and constant symbols

* removed the display parameter from kernel subproofs

* Removed display option from subproof. Add back the missing RewriteTrue case in the printer. Correct issue with equivalence checker.

* scalafix

New tactic system
Proofs can now be written using dedicated tactics and deduced steps. Tactics can be developped as object from which a SCProof can be recomputed.
Management of premises and target bottom sequent is unified, but tactics can optionally take other arguments.
Tactics can be used to construct proof using a dedicated syntax and DSL. Formally, The proof is built imperatively.
This means it is possible to write code in the middle of the proof (for example to print it) and it is possible to assign proof steps.
The library keep track of the proof being written from start to finish. A proof may look like:
```
THEOREM("fixedPointDoubleApplication") of "∀'x. 'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('f('x)))" PROOF {
        assume(forall(x, P(x) ==> P(f(x))))
        val base = have( (P(x) ==> P(f(x)), P(f(x)) ==> P(f(f(x)))) |- P(x) ==> P(f(f(x))))           by   Trivial
        have(() |- P(x) ==> P(f(f(x))))             by   SUBPROOF {
          have(P(f(x)) ==> P(f(f(x))) |- P(x) ==> P(f(f(x))) )                by   LeftForall(x)(base)
          andThen(() |- P(x) ==> P(f(f(x))))              by   LeftForall(f(x))
        }
      }
```
Sequent Calculus proof steps have been adapted so that they need only the minimum (often zero) explicit parameters, whcih are automatically infered.
Subproofs can also be used, and there is no need to do import management. Imports of Justifications and of proof steps of enclosing proofs are
automatically passed through the imports.
User should not use integers anymore to refer to premises, but instead provide a previous proof step or a justification directly.
On top of basic sequent calculus steps, the naive propositional solver and a tactic to instantiate forall quantifiers.
Existing proof have been translated to old sequent calculus (with every step lead by SC.) to make room for the new tactics identifiers.

Change the statements of existing theorems accordingly: into expressions that
the parser can parse.

Proof Transformation: Utility to transform a conditional proof into an unconditional proof of a conditional statement. Move the imports to the left of the conclusion.

Print and/or connector formulas with 1 argument

* Change Iff.id to match Implies.id

* Recognize more arrows as iff / implies

* Update printer tests to use new Iff.id

Co-authored-by: Viktor Kunčak <vkuncak@users.noreply.github.com>

* Integration mostly but roughly finished. Code compiles and is adapted to the change of variables representation in the kernel, except for two parts:
Unification is not fully working. It is used in many "tactics" deduction rules, expect some of those to not always work.
Fornt Macro: Compile-time string interpolation, with quote and so on. Probably easier to correct, but the syntax of that code is very difficult to understand. Dor now, this functionality is disabled (commented).

* simplifying, completting and consitentifying representations of schematic nodes in the Kernel. For now, Kernel compiles.

* More consistency and completeness changes. Code compile and tests outside the front do pass. Some tests related to unification and rules application in the front don't.

* Scaladoc up to date for the whole kernel.

* Removed the singleton set symbol from the definition of set theory. It should be an easily derived symbol. Added the missing subset axiom to set theory. Improved documentation for RunningTheory and Set Theory.

* Added a new deduction step: Rewrite True. it subsumes Hypothesis and is equivalent to rewriting a sequent that is OCBSL-true. Added top and bot constant predicate labels. Some more documentation.

* Rework of the user manual. Contains about everything Kernel-related. Does not contain documentation about the front, nor about the example development.

* Commented a test that can't pass until the unifier is repaired.

* remove leftover tentative code in Mapping.scala

* Make unification tests more readable:
* improve error messages when a test fails
* name emptyContext and emptyResult instead of using UnificationContext()
* split the expected unification result into a separate clause
  in the method to distinguish visually checkDoesNotUnify(a, b, partial)
  and checkUnifiesAs(a, b, expected)

* Split unification tests into multiple test cases

* @Ignore front's proof tests (instead of commenting out)

* Improve error messaging in front ProofTests

In particular, supply clues when assertions fail and split the tests into
test cases to clearly see which tests pass and which fail.

* Ignore unification tests until unification works with the new version of Lisa

* Run scalafix

* Further split unification tests: 1 test corresponds to 1 check

* Merge conflicts in the manual

* scalafix.

* scalafix 2.

* scalafix 3.

* trying to sastisfy the CI 5.

* Trying to satisfy the CI, 6.

* Trying to satisfy the CI, 7.

* Trying to satisfy the CI, 8.

* Front integration (#52)

* Large update to the user manual
* Merge development in Peano Arithmetic

* scalafix.

* Front integration (#53)

Reintroduce all of the front. 
Make the parser and printer working with the change on FOL..
Compatibility with the Peano Arithmetic development.
Update to the Manual.

Co-authored-by: Katja Goltsova <katja.goltsova@protonmail.com>

* When an unexpected token is encountered, add the string representation of the token
to the exception
* When printing of a sequent / formula / term fails, try to identify the smallest structure
on which the printing fails by attempting to print all subformulas and subterms. Report that
printing failed on the smallest structure rather than on the whole sequent / formula / term.

Represented as And() and Or() respectively.

Simply print the formula and expect it to be equal to the string
instead of parsing the string and expecting it to be equal to the
formula. Not all tests of the parser are tests for printer, because
there exist multiple strings that correspond to the same formula
(due to extra parentheses and multiple ways to write connectors).

* equality does not have to be parenthesized
* 'and' has higher priority than 'or', so parentheses are not needed to express order
* '∀ ?x.' instead of '∀x.'

Add inverse functions for all parsing rules. Further simplify parsing
of binder formulas and factor out toplevel (iff, implies) connector
formulas to make printing implementation easier.

Add tests for sequent parsing.

Implement a parser for first order logic with equality and schematic functions/predicates
using scallion.