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.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.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isTwoPow {w : Nat} (x : BitVec w) : Option Nat

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isTwoPow x = if (x == 0#w) = true then none else Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isTwoPow.go x 0

@[irreducible]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isTwoPow.go {w : Nat} (x : BitVec w) (counter : Nat) : Option Nat

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.bv_elim_ushiftRight_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_elim_shiftLeft_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_concat_extract : Meta.Simp.Simproc

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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