This module contains the implementation of the and flattening pass in the fixpoint pipeline, taking hypotheses of the form h : x && y = true and splitting them into h1 : x = true and h2 : y = true recursively.

structure Lean.Elab.Tactic.BVDecide.Frontend.Normalize.AndFlattenState : Type

• hypsToDelete : Array FVarId
• hypsToAdd : Array Meta.Hypothesis
• cache : Std.HashSet Expr

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

Flatten out ands. That is look for hypotheses of the form h : (x && y) = true and replace them with h.left : x = true and h.right : y = true. This can enable more fine grained substitutions in embedded constraint substitution.

Equations

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