This module contains the implementation of the associativity and commutativity normalisation pass in the fixpoint pipeline.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.acNormalizePass : Pass

Normalize with respect to Associativity and Commutativity.

Equations

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