Substitutions (#84)
* 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.
Showing
- lisa-examples/src/main/scala/Example.scala 1 addition, 0 deletionslisa-examples/src/main/scala/Example.scala
- lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala 67 additions, 57 deletions...l/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
- lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala 0 additions, 3 deletions...kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
- lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala 10 additions, 0 deletionslisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
- lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala 1 addition, 0 deletions...s/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
- lisa-utils/src/main/scala/lisa/utils/tactics/ProofsHelpers.scala 8 additions, 0 deletions...ils/src/main/scala/lisa/utils/tactics/ProofsHelpers.scala
- lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala 6 additions, 5 deletions...rc/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala
- src/main/scala/lisa/automation/kernel/SimpleSimplifier.scala 208 additions, 0 deletionssrc/main/scala/lisa/automation/kernel/SimpleSimplifier.scala
Loading
Please register or sign in to comment