Skip to content

New substitution mechanism

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

Created by: SimonGuilloud

  • "Function like"-terms and formulas, now have a specific syntax.
  • The arguments of those functions are now nullary schemas rather than variables
  • RightSubstEq, LeftSubstEq, RightSubstIff and LeftSubstIff now accepts arbitrarily many pairs of terms or formulas, i.e. they can do simultaneous substitutions of many pairs of terms or formulas
  • InstFunSchema and InstPredSchema now allows to instantiate arbitrarily many schematic symbols as well.

This implies a lots of syntax change on existing code, elthough it is mostly systematic. All proofs have been adapted to this new syntax.

Merge request reports