Documentation

Lean.Elab.Tactic.BVDecide.Frontend.Normalize.ShortCircuit

This module contains the implementation of the short-circuiting pass, which is responsible for applying short-circuit optimizations for *, e.g., translating x1 * y == x2 * y to !(!x1 == x2 && !x1 * y == x2 * y).

Responsible for applying short-circuit optimizations for *, e.g., translating x1 * y == x2 * y to !(!x1 == x2 && !x1 * y == x2 * y).

Equations
  • One or more equations did not get rendered due to their size.
Instances For