aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/Toplevel2.v
Commit message (Expand)AuthorAge
* WIPGravatar jadep2019-01-03
* remove dead codeGravatar jadep2019-01-03
* remove whitespace, print statements, and some dead tacticsGravatar jadep2019-01-03
* fixed up some of the fancy rewrite rulesGravatar jadep2019-01-03
* WIP: prove that barrett_red256 is a valid expression modulo some issues with ...Gravatar jadep2019-01-03
* WIP: expand valid_ident and prove of_prefancy_correct using itGravatar jadep2019-01-03
* WIP : made everything more concrete and proved of_Expr. Still to do for of_Ex...Gravatar jadep2019-01-03
* WIPGravatar jadep2019-01-03
* WIPGravatar jadep2019-01-03
* WIPGravatar jadep2019-01-03
* WIPGravatar jadep2019-01-03
* Guarantee that casting always returns inrangeGravatar Jason Gross2018-10-12
* Support type variables in patterns in the rewriterGravatar Jason Gross2018-09-29
* Fix proofs broken by changes to cc_m proofsGravatar Jason Gross2018-08-24
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Fix another proof broken by wrong behavior of cbnGravatar Jason Gross2018-08-14
* Fix a proof broken by wrong behavior of cbnGravatar Jason Gross2018-08-14
* Finish AbsInt Wf proofsGravatar Jason Gross2018-08-04
* Integrate Wf and Interp proofsGravatar Jason Gross2018-07-30
* Better error message printingGravatar Jason Gross2018-07-12
* Add support for annotating generated C functions with commentsGravatar Jason Gross2018-07-03
* synthesize squareGravatar Jason Gross2018-07-03
* WIPGravatar Jason Gross2018-07-03
* Add another prime exampleGravatar Jason Gross2018-06-18
* New pipeline, split among filesGravatar Jason Gross2018-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 19:12:25 +0000