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.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.andFlatteningPass.processGoal (goal : MVarId) : StateRefT' IO.RealWorld AndFlattenState MetaM Unit

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.andFlatteningPass.processFVar (fvar : FVarId) : StateRefT' IO.RealWorld AndFlattenState MetaM Unit

Equations

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

partial def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.andFlatteningPass.splitAnds (worklist : List Meta.Hypothesis) : StateRefT' IO.RealWorld AndFlattenState MetaM Unit

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.andFlatteningPass.trySplit (hyp : Meta.Hypothesis) : StateRefT' IO.RealWorld AndFlattenState MetaM (Option (Meta.Hypothesis × Meta.Hypothesis))

Equations

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