Skip to content
Snippets Groups Projects
  • SimonGuilloud's avatar
    72ff24fc
    Set2 (#126) · 72ff24fc
    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
    Set2 (#126)
    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