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

chore: remove use of deprecated API (#8970)

Browse source
This commit is contained in:
Henrik Böving 2025-06-24 10:22:50 +02:00 • committed by GitHub
parent 46a7c9108f
commit a223e92f85
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/BitVec/Bootstrap.lean
View file

@ -75,7 +75,7 @@ theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
cases b <;> trivial
· have p1 : i ≠ n := by omega
have p2 : i - n ≠ 0 := by omega
simp [p1, p2, Nat.testBit_bool_to_nat]
simp [p1, p2, Nat.testBit_bool_toNat]
private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_right (by trivial : 0 < 2) le)

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

@ -3062,7 +3062,7 @@ theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
cases b <;> trivial
· have p1 : i ≠ n := by omega
have p2 : i - n ≠ 0 := by omega
simp [p1, p2, Nat.testBit_bool_to_nat]
simp [p1, p2, Nat.testBit_bool_toNat]
@[simp] theorem msb_cons : (cons a x).msb = a := by
simp [cons, msb_cast, msb_append]