Skip to content

Various corrections, new set theory development as better examples.

Viktor Kuncak requested to merge github/fork/SimonGuilloud/main into main

Created by: SimonGuilloud

  • Added kernel helper functions to instantiate schematic predicate or function in a whole sequent
  • Corrected equivalence checker to deal correctly with empty disjunction (permits among other to use True and False in Rewrite)
  • Inconsequential change in a small helper method "bindAll" so that it doesn't sort variables
  • Small qol update in the function symbol definition in the running theory so that when verifying the definition of a new symbol, it checks the formulas with variables bound from left to right and from right to left.
  • InstFunSchema and InstPredSchema weren't extending SCProofStep
  • Corrected minor issues with axiom files of set theory (SetTheoryZAxioms, etc)
  • New file with some development of set theory, in particular theorems regarding mapping/replacement on sets and cartesian product.
  • Completed ElementsOfSetTheory so that it fills an actual theory.
  • Improvement/Correction of various "tactics".

Merge request reports