index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Arithmetic
/
Core.v
Commit message (
Expand
)
Author
Age
*
update _CoqProject, fix indentations, and prune dependencies of new Arithmeti...
jadep
2019-04-03
*
split up Arithmetic (imports etc. not yet fixed, does not build)
jadep
2019-04-03
*
remove old pipeline
Andres Erbsen
2019-01-09
*
Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil
Jason Gross
2018-08-23
*
Move chained_carries' (now chained_carries_reduce)
Jason Gross
2017-11-07
*
Split off computational part of basesystem_partial_evaluation_RHS_gen
Jason Gross
2017-11-07
*
More use of Z.eqb_cps
Jason Gross
2017-11-07
*
Use div_cps and modulo_cps in more places
Jason Gross
2017-11-07
*
Make use of id_tuple_with_alt_cps'
Jason Gross
2017-11-06
*
Make use of from_associational_cps in more places
Jason Gross
2017-11-01
*
More use of Z.eqb_cps
Jason Gross
2017-11-01
*
Add another unfolding database
Jason Gross
2017-10-22
*
Use fold_right_cps2 to get eqb_cps to get the right continuation type
Jason Gross
2017-10-19
*
Switch arithmetic to cps for Z * Z under the hood
Jason Gross
2017-10-19
*
Pattern over cps lemmas in Arithmetic/Core
Jason Gross
2017-10-19
*
Unfold more things in basesystem_partial_evaluation_unfolder
Jason Gross
2017-10-18
*
Add some more things to basesystem_partial_evaluation_unfolder
Jason Gross
2017-10-18
*
Add basesystem_partial_evaluation_unfolder db
Jason Gross
2017-10-18
*
Allow instantiating type arguments without reducing matches
Jason Gross
2017-10-18
*
Pattern more things in arithmetic/core
Jason Gross
2017-10-17
*
Add MulSplitUnfolder
Jason Gross
2017-10-17
*
Add faster arithmetic unfolding
Jason Gross
2017-10-15
*
Extend basesystem_partial_evaluation_RHS
Jason Gross
2017-10-15
*
Fix a typo in the previous commit
Jason Gross
2017-10-14
*
Split up solve_op_mod_eq
Jason Gross
2017-10-14
*
Add cbv_runtime in Arithmetic/Core
Jason Gross
2017-07-08
*
Add nonzero synthesis
Jason Gross
2017-06-26
*
define strong small and re-prove small_add and small_compact with that defini...
jadep
2017-06-18
*
Improve replace_match_with_destructuring_match
Jason Gross
2017-06-15
*
Don't rely on autogenerated names
Jason Gross
2017-06-05
*
export a few more wrapper definitions in Positional
jadep
2017-06-02
*
Strip trailing whitespace
Jason Gross
2017-06-02
*
force carry intermediates to be bound early
Andres Erbsen
2017-05-14
*
make freeze use the correct versions of add_get_carry and zselect
jadep
2017-05-14
*
move some lemmas to Core and define a tuple-select operation
jadep
2017-05-01
*
stricter divmod proofs
jadep
2017-05-01
*
rename-everything
Andres Erbsen
2017-04-06