issues
search
mit-plv
/
bbv
Bedrock Bit Vector Library
MIT License
27
stars
23
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Adapt to https://github.com/coq/coq/pull/19530
#51
proux01
opened
1 month ago
0
New release for Coq 8.19?
#50
MackieLoeffel
closed
7 months ago
2
adapt to coq/coq#18730
#49
andres-erbsen
closed
8 months ago
0
need coq 8.18 compatible release
#48
vzaliva
closed
1 year ago
4
Remove deprecated files in Coq.Arith
#47
Villetaneuse
closed
1 year ago
12
Incompatibility with coq.8.17.1
#46
ric-almeida
opened
1 year ago
1
Stop using auto with * in intuition
#45
SkySkimmer
opened
1 year ago
0
Adapt w.r.t. coq/coq#16903.
#44
ppedrot
closed
1 year ago
1
Adapt to coq/coq#16920
#43
olaure01
closed
1 year ago
0
Adapt w.r.t. coq/coq#16904.
#42
ppedrot
closed
1 year ago
0
Alternate adaptation w.r.t. coq/coq#16004
#41
JasonGross
closed
2 years ago
5
Adapt w.r.t. coq/coq#16004.
#40
ppedrot
closed
2 years ago
8
Test more released versions of Coq
#39
JasonGross
closed
2 years ago
0
Make new 8.14 compatible release
#38
skeuchel
closed
2 years ago
2
Avoid unary round-trip for binary literals
#37
bacam
closed
3 years ago
0
Adapt to coq/coq#14819
#36
proux01
closed
3 years ago
0
modify pow2_inc
#35
thery
closed
3 years ago
0
Future proof NatLib and ZLib
#34
mrhaandi
closed
3 years ago
0
Make bbv compatible with Coq 8.7
#33
JasonGross
closed
3 years ago
2
Make some uses of `apply` more robust
#32
maximedenes
closed
4 years ago
0
compatibility with Coq PR #11906
#31
fajb
closed
4 years ago
1
Make explicit which hint databases to use with firstorder
#30
JasonGross
closed
4 years ago
0
Update gitignore for compatibility with Coq master
#29
tchajed
closed
5 years ago
0
Enable travis
#28
JasonGross
closed
5 years ago
0
Allow use of bbv with COQPATH
#27
JasonGross
closed
5 years ago
0
Compatibility with PR #9725
#26
fajb
closed
5 years ago
3
Update opam package
#25
gmalecha
closed
3 years ago
8
compatibility with coq 8.9
#24
gmalecha
closed
5 years ago
2
Proved the idempotent property for wor.
#23
llee454
opened
5 years ago
0
bulky representation of concrete words
#22
aa755
opened
6 years ago
2
Building theories/Word.vo is slow
#21
JasonGross
opened
6 years ago
9
Export String in {Bin,Hex}Notation
#20
JasonGross
closed
6 years ago
0
Remove trailing spaces
#19
Columbus240
closed
6 years ago
1
make notation point to transparent versions of bitshift.
#18
gmalecha
closed
6 years ago
1
minimal changes needed to make omega an alias for lia
#17
samuelgruetter
closed
6 years ago
2
Make an opam package
#16
gmalecha
closed
6 years ago
7
fix implicit arguments in bitshift notation.
#15
gmalecha
closed
6 years ago
1
Prepare porting from omega to lia
#14
maximedenes
closed
6 years ago
0
Move notations to their own modules
#13
JasonGross
closed
6 years ago
1
Makefile as per suggestions by others
#12
vmurali
closed
6 years ago
11
Extracting [hexDigitToN] in Haskell creates Data.Bits.testBit and Data.Char.ord
#11
vmurali
opened
6 years ago
1
bbv/theories checkin breaks all projects using bbv
#10
vmurali
closed
6 years ago
2
mostly cosmetic changes
#9
gmalecha
closed
6 years ago
22
add lemmas about ZToWord and about natToWord and mod
#8
samuelgruetter
closed
6 years ago
0
got rid of Psatz
#7
vmurali
closed
6 years ago
1
Word lemmas depend on real number axioms
#6
samuelgruetter
closed
6 years ago
4
bbv makes it impossible to use $ as a prefix printing notation without parentheses
#5
JasonGross
closed
6 years ago
15
Add nice properties for natToWord (sz+1) (pow2 sz)
#4
pedrotst
closed
6 years ago
0
Nice properties of natToWord (sz+1) (pow2 sz)
#3
pedrotst
closed
6 years ago
0
Migrate WordProps from Kami
#2
pedrotst
closed
6 years ago
0
Next