Documentation

Std.Tactic.BVDecide.Normalize.BitVec

This module contains the BitVec simplifying part of the bv_normalize simp set.

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_sshiftRight {w : Nat} {a : Nat} :
(0#w).sshiftRight a = 0#w
theorem Std.Tactic.BVDecide.Normalize.BitVec.sshiftRight_zero :
∀ {w : Nat} {a : BitVec w}, a.sshiftRight 0 = a
theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_ult' {w : Nat} (a : BitVec w) :
(0#w).ult a = (0#w != a)
theorem Std.Tactic.BVDecide.Normalize.BitVec.getElem_eq_getLsbD {w : Nat} (a : BitVec w) (i : Nat) (h : i < w) :
a[i] = a.getLsbD i