epfl-lara/lisa

Issues

• Null pointer exception raised when variable has not yet been declared

  #218 opened 6 months ago by agilot
  1

• Substitution tactic crashes when assumptions are not complete

  #215 opened 7 months ago by SimonGuilloud
  0

• Substitution.ApplyRules error

  #214 opened 7 months ago by SimonGuilloud
  0

• Unsealed `Proof` class

  #190 opened 10 months ago by sankalpgambhir
  1

• `sbt assembly` doesn't actually work

  #188 opened 10 months ago by sankalpgambhir
  1

• It should be possible to export and import LISA proofs into and from text files.

  #76 opened 10 months ago by SimonGuilloud
  1

• Use string interpolation to specify formulas partially as strings and partially as scala code

  #77 opened a year ago by SimonGuilloud
  2

• `Restate` type alias raises errors

  #119 opened 2 years ago by sankalpgambhir
  2

• Assumption handling (or lack thereof) in presence of imports

  #161 opened a year ago by sankalpgambhir
  0

• `InstantiateForall` overloading errors

  #120 opened a year ago by sankalpgambhir
  2

• `repr` fails on a `null` match on encountering a wrong theorem

  #157 opened a year ago by sankalpgambhir
  0

• Make the propositional prover use the equivalence checker

  #78 opened 2 years ago by SimonGuilloud
  0

• Wrong error messages for definitions with mismatched proofs

  #129 opened 2 years ago by sankalpgambhir
  0

• Front macro is not working anymore

  #38 opened 2 years ago by SimonGuilloud
  0

• Adopt the convention that axioms and theorems don't have top-level universal quantifiers on the right and existential quantifiers on the left

  #79 opened 2 years ago by SimonGuilloud
  1

• Repair and improve the unifier

  #37 opened 2 years ago by SimonGuilloud
  0

• Failed `require`s give unhelpful (and uncaught) errors

  #110 opened 2 years ago by sankalpgambhir
  2

• Print errors from parsing in a meaningful way

  #86 opened 2 years ago by SimonGuilloud
  4

• Print errors from proof tactics in meaningful way

  #85 opened 2 years ago by SimonGuilloud
  2

• New tactic trait system interferes with overload resolution

  #100 opened 2 years ago by sankalpgambhir
  1

• Printer and Parser should allow unicode aliases for symbols

  #75 opened 2 years ago by SimonGuilloud
  0

• Printer fails on SchematicConnectorLabels

  #81 opened 2 years ago by lighthea
  0

• Left-hand side does not contain formula φ

  #98 opened 2 years ago by pgimalac
  3

• Equivalence checker deals incorrectly with labels

  #74 opened 2 years ago by SimonGuilloud
  1

• instantiatePredicateSchemas does not instantiates VariableFormulaLabels

  #80 opened 2 years ago by lighthea
  1

• Creat a minimal tactic system for the kernel

  #49 opened 2 years ago by SimonGuilloud
  0

• Assertions on which theorem is proven

  #9 opened 2 years ago by vkuncak
  1

• Integration of the front

  #34 opened 2 years ago by FlorianCassayre
  1

• Documentation needs updating

  #36 opened 2 years ago by SimonGuilloud
  1

• Loading the project fails in Intellij Idea

  #69 opened 2 years ago by cache-nez
  0

• Parser failing on single argument Or/And formula

  #60 opened 2 years ago by lighthea
  3

• Missing definitions in set theory

  #10 opened 2 years ago by FlorianCassayre
  2

• Isabelle tactic for Lisa proofs

  #23 opened 2 years ago by vkuncak
  1

• More testing cases for the Kernel

  #39 opened 2 years ago by SimonGuilloud
  0

• Equivalence checker is not symmetric

  #12 opened 2 years ago by FlorianCassayre
  4

• It is not possible to do partial substitution

  #5 opened 2 years ago by SimonGuilloud
  2