max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: delete double namespace BitVec.BitVec (#4165)

Browse source 
Fixes double namespace introduced in #4148
This commit is contained in:
Siddharth 2024-05-14 20:34:14 +01:00 • committed by GitHub
parent f3538dbdfa
commit 367b97885a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/BitVec/Lemmas.lean
View file

@ -609,7 +609,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
(shiftLeftZeroExtend x i).msb = x.msb := by
simp [shiftLeftZeroExtend_eq, BitVec.msb]
theorem BitVec.shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
(x <<< n) <<< m = x <<< (n + m) := by
ext i
simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and]
@ -705,7 +705,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
simp only [getLsb_append, cond_eq_if]
split <;> simp [*]
theorem BitVec.shiftRight_shiftRight (w : Nat) (x : BitVec w) (n m : Nat) :
theorem shiftRight_shiftRight (w : Nat) (x : BitVec w) (n m : Nat) :
(x >>> n) >>> m = x >>> (n + m) := by
ext i
simp [Nat.add_assoc n m i]