This module contains implementations of simprocs used in the bv_normalize simp set.

structure Lean.Meta.Tactic.BVDecide.Normalize.OpCache : Type

• oneWidthCache : Std.HashMap (Sym.ExprPtr × Name) Expr
• extractCache : Std.HashMap (Sym.ExprPtr × Sym.ExprPtr × Sym.ExprPtr) Expr
• appendCache : Std.HashMap (Sym.ExprPtr × Sym.ExprPtr × Sym.ExprPtr) Expr
• statistics : Std.HashMap Name Nat

  How often each rewrite subrule fired.

def Lean.Meta.Tactic.BVDecide.Normalize.rewriteSimproc (cache : ST.Ref IO.RealWorld OpCache) : Sym.Simp.Simproc

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.rewriteSimproc cache e = Lean.Meta.Tactic.BVDecide.Normalize.rewriteSimproc.go✝ e cache

def Lean.Meta.Tactic.BVDecide.Normalize.rewriteDsimproc : Sym.DSimp.DSimproc

Equations

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