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.

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

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

Instances For

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

Instances For