This modules contains simprocs and functions to compute discrimination tree keys in order to construct simp sets that apply `apply_ite` and `Bool.apply_cond` to specific functions.

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.applyIteSimproc :
Meta.Simp.Simproc
Equations

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

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.applyCondSimproc :
Meta.Simp.Simproc
Equations

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

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.mkApplyProjControlDiscrPath (struct : Name) (structParams projIdx : Nat) (controlFlow : Name) (controlFlowParams : Nat) :
Array Meta.DiscrTree.Key

For `Prod.fst` and `ite` this function creates the path: `Prod.fst (ite (Prod _ _) _ _ _ _)`. This path can be used to match on applications of structure projections onto control flow primitives.

Equations

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

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.mkApplyUnaryControlDiscrPath (type : Name) (typeParams : Nat) (constName controlFlow : Name) (controlFlowParams : Nat) :
Array Meta.DiscrTree.Key

For `f`, `SomeType α β` and `ite` this function creates the path: `f (ite (SomeType _ _) _ _ _ _)`. This path can be used to match on applications of unary functions onto control flow primitives.

Equations

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

Instances For