aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/Core.v
Commit message (Expand)AuthorAge
* Add cbv_runtime in Arithmetic/CoreGravatar Jason Gross2017-07-08
* Add nonzero synthesisGravatar Jason Gross2017-06-26
* define strong small and re-prove small_add and small_compact with that defini...Gravatar jadep2017-06-18
* Improve replace_match_with_destructuring_matchGravatar Jason Gross2017-06-15
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* export a few more wrapper definitions in PositionalGravatar jadep2017-06-02
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* force carry intermediates to be bound earlyGravatar Andres Erbsen2017-05-14
* make freeze use the correct versions of add_get_carry and zselectGravatar jadep2017-05-14
* move some lemmas to Core and define a tuple-select operationGravatar jadep2017-05-01
* stricter divmod proofsGravatar jadep2017-05-01
* rename-everythingGravatar Andres Erbsen2017-04-06