-
SimonGuilloud authored
* Redoing to proofs in SetTheory2 (pairs symmetry and deconstruction). Making some improvements to applySubst * Changed axioms of lisa.settheory to be actual Axiom instead of Formulas. Changed some details un subproof. * Corrected applySubst. Create a new error for ill-defined axioms. New helper function to add axioms. * Corrected issue where every time an "axiom" was given to a tactic, it was actually a formula, often cast implicitely to an axiom at runtime. * all compiles and tests passes * Corrected issue with overloading failing. * reduced proof on unordered pairs deconstruction. * correct abusive refactor
SimonGuilloud authored* Redoing to proofs in SetTheory2 (pairs symmetry and deconstruction). Making some improvements to applySubst * Changed axioms of lisa.settheory to be actual Axiom instead of Formulas. Changed some details un subproof. * Corrected applySubst. Create a new error for ill-defined axioms. New helper function to add axioms. * Corrected issue where every time an "axiom" was given to a tactic, it was actually a formula, often cast implicitely to an axiom at runtime. * all compiles and tests passes * Corrected issue with overloading failing. * reduced proof on unordered pairs deconstruction. * correct abusive refactor
Example.scala 4.87 KiB