Repository navigation

feat: wide fixed-width integer load/store accessors on ByteArray - #14053

Draft

kim-em wants to merge 8 commits into

leanprover:masterfrom

kim-em:bytearray-wide-uint-accessors

Draft

feat: wide fixed-width integer load/store accessors on ByteArray#14053
kim-em wants to merge 8 commits into
leanprover:masterfrom
kim-em:bytearray-wide-uint-accessors

Commits on Jun 15, 2026
- feat: wide fixed-width integer load/store accessors on ByteArray
  
  kim-em
  and
  claude
  committed
  ce55a45
Commits on Aug 26, 2026
- chore: remove empty bytearray_pack.lean.out.expected
  Kim Morrison
  committed
  a9687de
- Merge remote-tracking branch 'origin/master' into bytearray-wide-uint-accessors
  Kim Morrison
  committed
  b1e5564
- refactor: move wide-accessor lemmas to Init.Data.ByteArray.Pack.Lemmas
  Kim Morrison
  committed
  5f9b9ae
- fix: restore the tactic and Array imports the moved lemmas relied on
  Kim Morrison
  committed
  00c99b9
- chore: if_pos was deprecated in favour of ite_eq_left
  Kim Morrison
  committed
  0c7cb7b
Commits on Oct 2, 2026
- Merge master into bytearray-wide-uint-accessors
  
  kim-em
  and
  claude
  committed
  6729f6e
Commits on Oct 6, 2026
- fix: use lean_sarray_ensure_exclusive in wide ByteArray setters
  
  kim-em
  and
  claude
  committed
  ae6bd28