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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.mkPow (x y : Expr) : MetaM Expr

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.mkPow x y = Lean.Meta.mkAppM `HPow.hPow #[x, y]

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

Equations

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