aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Remove nested proofsGravatar Jason Gross2018-07-03
|
* Fix hints, hopefullyGravatar Jason Gross2018-07-03
|
* cleanGravatar Jason Gross2018-07-03
|
* Finish reduce_square proofGravatar Jason Gross2018-07-03
|
* update cGravatar Jason Gross2018-07-03
|
* Try to fix square againGravatar Jason Gross2018-07-03
|
* update cGravatar Jason Gross2018-07-03
|
* Fix a typo, start on proofGravatar Jason Gross2018-07-03
|
* update cGravatar Jason Gross2018-07-03
|
* Fix a reification issueGravatar Jason Gross2018-07-03
|
* Try a different reduce_squareGravatar Jason Gross2018-07-03
|
* WIP better squareGravatar Jason Gross2018-07-03
|
* Add generated .c filesGravatar Jason Gross2018-07-03
|
* Fix missing argGravatar Jason Gross2018-07-03
|
* Add missing spaceGravatar Jason Gross2018-07-03
|
* Add support for annotating generated C functions with commentsGravatar Jason Gross2018-07-03
| | | | As requested by @davidben (though I haven't yet written any comments for the functions)
* Synthesize selectznzGravatar Jason Gross2018-07-03
|
* Correctly reify match on prodGravatar Jason Gross2018-07-03
|
* Add selectGravatar Jason Gross2018-07-03
|
* Comment out some code that's too slowGravatar Jason Gross2018-07-03
|
* Synthesize moreGravatar Jason Gross2018-07-03
|
* Allow passing functions to synthesize on the command line, and scmul for 25519Gravatar Jason Gross2018-07-03
|
* Pull out *2 in square, don't turn *2 into <<1Gravatar Jason Gross2018-07-03
|
* No subst01 in mulmodGravatar Jason Gross2018-07-03
|
* Start with a better template for carry_squareGravatar Jason Gross2018-07-03
|
* Don't subst01 in squareGravatar Jason Gross2018-07-03
|
* synthesize squareGravatar Jason Gross2018-07-03
|
* static in cGravatar Jason Gross2018-07-03
|
* static voidGravatar Jason Gross2018-07-03
|
* WIPGravatar Jason Gross2018-07-03
|
* Add ZUtil, list lemmasGravatar Jason Gross2018-07-02
|
* Fix a notation issue in previous commitGravatar Jason Gross2018-07-02
|
* Add more ListUtil proofsGravatar Jason Gross2018-07-02
|
* Add some list lemmasGravatar Jason Gross2018-07-02
|
* Make all parameters implicitGravatar Jasper Hugunin2018-07-02
|
* Prefer relations of the form [eq ==> eq ==> ... ==> eq] in setoidsGravatar Jason Gross2018-07-01
| | | | Also make it easy to redeclare such instances.
* Add useful list lemmasGravatar Jason Gross2018-06-29
|
* Add ZUtil.SortingGravatar Jason Gross2018-06-29
|
* Revert "Add more schemes for prod"Gravatar Jason Gross2018-06-28
| | | | | | This reverts commit 5d38a03f5a9f69a78a582cc9cc1c350dc6596cd3. Some of these already exist in Datatypes
* Add more schemes for prodGravatar Jason Gross2018-06-28
|
* Remove useless RequiresGravatar Jason Gross2018-06-28
|
* Fix sed scripts in MakefileGravatar Jason Gross2018-06-28
|
* Try out stronger land, lor boundsGravatar Jason Gross2018-06-27
|
* Add is_tighter_than_bool lemmasGravatar Jason Gross2018-06-27
|
* Add lnot mod pull/push lemmasGravatar Jason Gross2018-06-27
|
* Add missing Z.lnot_0 hintsGravatar Jason Gross2018-06-27
|
* Add more Z const hintsGravatar Jason Gross2018-06-27
|
* Remove lneg in favor of lnot_modulo (lneg was wrong)Gravatar Jason Gross2018-06-27
|
* Add some Z.land, Z.lor hintsGravatar Jason Gross2018-06-27
|
* Add a couple of zrange lemmasGravatar Jason Gross2018-06-26
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 07:41:15 +0000