Skip to content

[Quant] Substitute by prefering existing terms to new equal one

François Bobot requested to merge bobot/abs into master

Avoid useless reasonning: - congruence closure - simplex - instantiations

  • Remove the hack about coercions that was just removing problematic axioms
  • Add definition folding
  • Fix propagation square root sign

Merge request reports