-
- Downloads
Atomics, improve lisa.fol.FOL's logic and simplify it (#194)
* Renamed some elements of the formula hierarchy using the word "atomic" * removed the match type for ***. Instead, use opaque types and extension methods. Should be a bit more efficient and less prone to dotty bugs * remove ***. Only ** left * removing apply for sequences (use applyUnsafe) * mostly good but one theorem doesn't pass anymore * everything goes, no more *** (i.e. no match type) * progress * PredKer * mend * ConstantAtomicLabel, AtomicFormula * All atomic renaming completed * back to compile * finished tests, removed ConsOrPred * next step: Removes contravariant labels and terms and formulas extending |-> * finish predicates, compiles * progress, Binders to sort and organize, some renaming to do in other files. Can remove - in labels. * finished cleaning and uniformizing definitions in Commons.scala, adapted other files accordingly. Compiles, tests passes, formated. * re-checked some warning, removed some redundant type checks. * fix substituteUnsafe2 * Add "lisa-sets / compile" and "lisa-examples / compile" to the CI.
Showing
- .github/workflows/ci.yml 4 additions, 0 deletions.github/workflows/ci.yml
- Reference Manual/kernel.tex 8 additions, 8 deletionsReference Manual/kernel.tex
- Reference Manual/lisa.pdf 0 additions, 0 deletionsReference Manual/lisa.pdf
- Reference Manual/shortcuts.tex 1 addition, 1 deletionReference Manual/shortcuts.tex
- lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala 13 additions, 13 deletions...l/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
- lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala 15 additions, 15 deletions...l/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
- lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala 8 additions, 8 deletions.../main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
- lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala 12 additions, 12 deletions...kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
- lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala 13 additions, 13 deletions...rnel/src/main/scala/lisa/kernel/proof/RunningTheory.scala
- lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala 7 additions, 7 deletions...nel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
- lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala 1 addition, 1 deletion...el/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
- lisa-sets/src/main/scala/lisa/SetTheoryLibrary.scala 1 addition, 1 deletionlisa-sets/src/main/scala/lisa/SetTheoryLibrary.scala
- lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala 24 additions, 21 deletionslisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
- lisa-sets/src/main/scala/lisa/automation/Substitution.scala 39 additions, 38 deletionslisa-sets/src/main/scala/lisa/automation/Substitution.scala
- lisa-sets/src/main/scala/lisa/automation/Tableau.scala 10 additions, 11 deletionslisa-sets/src/main/scala/lisa/automation/Tableau.scala
- lisa-sets/src/main/scala/lisa/automation/Tautology.scala 5 additions, 5 deletionslisa-sets/src/main/scala/lisa/automation/Tautology.scala
- lisa-sets/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala 1 addition, 1 deletion...in/scala/lisa/automation/settheory/SetTheoryTactics.scala
- lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala 1 addition, 1 deletion...s/src/main/scala/lisa/maths/settheory/InductiveSets.scala
- lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala 1 addition, 1 deletion...main/scala/lisa/maths/settheory/orderings/Recursion.scala
- lisa-sets/src/test/scala/lisa/examples/peano_example/PeanoArithmetics.scala 1 addition, 1 deletion.../scala/lisa/examples/peano_example/PeanoArithmetics.scala
Loading
Please register or sign in to comment