File tree Expand file tree Collapse file tree 1 file changed +4
-4
lines changed Expand file tree Collapse file tree 1 file changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -869,15 +869,15 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
869
869
(x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
870
870
rfl
871
871
872
- @[simp] theorem getLsb_append {v : BitVec n} {w : BitVec m} :
873
- getLsb (v ++ w ) i = bif i < m then getLsb w i else getLsb v (i - m) := by
872
+ @[simp] theorem getLsb_append {x : BitVec n} {y : BitVec m} :
873
+ getLsb (x ++ y ) i = bif i < m then getLsb y i else getLsb x (i - m) := by
874
874
simp only [append_def, getLsb_or, getLsb_shiftLeftZeroExtend, getLsb_zeroExtend']
875
875
by_cases h : i < m
876
876
· simp [h]
877
877
· simp [h]; simp_all
878
878
879
- @[simp] theorem getMsb_append {v : BitVec n} {w : BitVec m} :
880
- getMsb (v ++ w ) i = bif n ≤ i then getMsb w (i - n) else getMsb v i := by
879
+ @[simp] theorem getMsb_append {x : BitVec n} {y : BitVec m} :
880
+ getMsb (x ++ y ) i = bif n ≤ i then getMsb y (i - n) else getMsb x i := by
881
881
simp [append_def]
882
882
by_cases h : n ≤ i
883
883
· simp [h]
You can’t perform that action at this time.
0 commit comments