This module contains the implementation of the embedded constraint substitution pass in the fixpoint pipeline, substituting hypotheses of the form h : x = true in other hypotheses.

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

Substitute embedded constraints. That is look for hypotheses of the form h : x = true and use them to substitute occurrences of x within other hypotheses. Additionally this drops all redundant top level hypotheses.

Equations

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