aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/Saturated/AddSub.v
Commit message (Expand)AuthorAge
* Add more versions of basesystem_partial_evaluation_unfolderGravatar Jason Gross2017-11-07
* Switch arithmetic to cps for Z * Z under the hoodGravatar Jason Gross2017-10-19
* Add basesystem_partial_evaluation_unfolder dbGravatar Jason Gross2017-10-18
* Allow instantiating type arguments without reducing matchesGravatar Jason Gross2017-10-18
* Closed under the global contextGravatar Andres Erbsen2017-07-02
* proved small_sat_addGravatar jadep2017-07-01
* Prove saturated carrying-subtraction-chain correctGravatar jadep2017-07-01
* Prove saturated carrying-addition-chain correctGravatar jadep2017-06-30
* Reorganization of saturated arithmeticGravatar jadep2017-06-29