Documentation

Lean.Meta.Tactic.BVDecide.Normalize.ApplyControlFlow

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.Meta.Tactic.BVDecide.Normalize.applyIteSimproc (headSyms : Std.HashSet Name) :
Sym.Simp.Simproc
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.Tactic.BVDecide.Normalize.applyCondSimproc (headSyms : Std.HashSet Name) :
    Sym.Simp.Simproc
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For