Skip to content

feat: add BitVec container operations #11329

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
f64u wants to merge 19 commits into
base: master
Choose a base branch
from
Open

feat: add BitVec container operations #11329

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
4e7400f
add folds
f64u Nov 21, 2025
52f74f4
add conversions
f64u Nov 22, 2025
ca88f82
add count
f64u Nov 22, 2025
e786558
support BitVec.concat
f64u Nov 22, 2025
cc3a991
induction principle
f64u Nov 22, 2025
ef0baf8
some golfing
f64u Nov 22, 2025
491c773
fix
f64u Nov 22, 2025
e4e10de
map and zip operations
f64u Nov 22, 2025
83251b1
feat: add BitVec container operations
f64u Nov 23, 2025
7a64013
test: add fold operation tests
f64u Nov 23, 2025
4dda1d0
feat: bitvec concat induction
f64u Nov 24, 2025
620055c
fixes
f64u Nov 24, 2025
7faf83b
feat: add extern implementation for popcount
f64u Nov 27, 2025
4956668
golf
f64u Nov 27, 2025
bd2fc8d
typo
f64u Nov 29, 2025
09bca7a
feat: symmetric LE/BE API for BitVec conversions
f64u Dec 5, 2025
489177e
feat: add ByteArray conversions for BitVec
f64u Dec 5, 2025
e5ef2c2
wip
f64u Dec 7, 2025
df2d2b0
feat: bitvec <-> bytearray conversions + theory
f64u Dec 10, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions src/Init/Data/BitVec.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,3 +13,7 @@ public import Init.Data.BitVec.Bitblast
public import Init.Data.BitVec.Decidable
public import Init.Data.BitVec.Lemmas
public import Init.Data.BitVec.Folds
public import Init.Data.BitVec.Conversions
public import Init.Data.BitVec.Count
public import Init.Data.BitVec.Map
public import Init.Data.BitVec.Hamming
Loading
Loading