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).

def Lean.Meta.Tactic.BVDecide.Normalize.shortCircuitPass : Pass

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.