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.

source
def Lean.Elab.Tactic.BVDecide.Frontend.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.

Instances For