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.

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

Equations

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

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

Equations

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

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.

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.