index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Util
/
ZUtil.v
Commit message (
Expand
)
Author
Age
*
Add ZUtil lemma
Jason Gross
2016-10-17
*
Fix compatibility with sigT notation
Jason Gross
2016-10-10
*
Make Ztestbit_full
Jason Gross
2016-10-09
*
Fix Ztestbit_full database
Jason Gross
2016-10-09
*
Fix shiftr_spec_full
Jason Gross
2016-10-09
*
Add more to Ztestbit_full
Jason Gross
2016-10-09
*
Add a Ztestbit_full database
Jason Gross
2016-10-09
*
Stronger Ztestbit, convert_to_ztestbit
Jason Gross
2016-10-07
*
More zsimplify lemmas, stronger Ztestbit
Jason Gross
2016-10-07
*
Weaken hyps of lor_range, add it to zarith
Jason Gross
2016-10-07
*
Moved lemma to ZUtil and added an extra lemma jgross needed
jadep
2016-10-06
*
Add testbit_add_shiftl_full
Jason Gross
2016-10-06
*
Use zutil_arith for side-conditions in testbit
Jason Gross
2016-10-06
*
Add Z.pow_le_mono_{r,l} to zarith
Jason Gross
2016-10-06
*
Add a lemma to Ztestbit about large indices
Jason Gross
2016-10-06
*
More zsimplify lemmas
Jason Gross
2016-10-04
*
Add Zplus_minus to zsimplify
Jason Gross
2016-10-04
*
Weaken hyps of zutil lemma
Jason Gross
2016-10-04
*
Add a variant of add_shift_mod
Jason Gross
2016-10-04
*
Add ZUtil lemma
Jason Gross
2016-10-04
*
Add ZUtil lemma
Jason Gross
2016-10-04
*
Add Zmult_lt_compat_r to zarith
Jason Gross
2016-10-04
*
Prevent infinite loops by not dealing with 0 mod _
Jason Gross
2016-10-04
*
Handle 0 mod _ in push_Zmod
Jason Gross
2016-10-04
*
Handle ?x mod ?x in push_Zmod
Jason Gross
2016-10-04
*
Z.ltb_to_lt now also handles eqb
Jason Gross
2016-10-04
*
Reorganization, moving of lemmas to correct files, and 8.4 compatibility
jadep
2016-09-21
*
More 8.4 compatibility
jadep
2016-09-14
*
Moved lemmas to ZUtil
jadep
2016-09-13
*
Work around bug #5073 (lia)
Jason Gross
2016-09-07
*
More zarith
Jason Gross
2016-08-24
*
Fewer side-conditions on zsimplify
Jason Gross
2016-08-24
*
Fix a Hint Resolve typo
Jason Gross
2016-08-23
*
More ZUtil
Jason Gross
2016-08-23
*
More ZUtil
Jason Gross
2016-08-23
*
Add Z.rewrite_mod_small
Jason Gross
2016-08-19
*
More powerful Z.div_mod_to_quot_rem
Jason Gross
2016-08-19
*
More ZUtil
Jason Gross
2016-08-18
*
Add ZUtil
Jason Gross
2016-08-18
*
Add a ZUtil hint
Jason Gross
2016-08-18
*
Add some ZUtil lemmas and hints
Jason Gross
2016-08-18
*
Add versions of ZUtil lemmas without nonzero assumptions
Jason Gross
2016-08-18
*
Add Z.opp_involutive to Zshift_to_pow
Jason Gross
2016-08-18
*
Add a ZUtil hint
Jason Gross
2016-08-17
*
Add Z.div_mod_to_quot_rem
Jason Gross
2016-08-17
*
Add [Z.linear_solve_for], [Z.linear_substitute]
Jason Gross
2016-08-17
*
More zsimplify
Jason Gross
2016-08-16
*
Add a faster zsimplify database
Jason Gross
2016-08-16
*
Merge of conversion development branch with master
jadep
2016-08-16
|
\
|
*
Moved Z lemmas useful for conversion proofs (mostly about bitwise operations)...
jadep
2016-08-16
[next]