aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/RewriterProofs.v
Commit message (Expand)AuthorAge
* Finish rewriter proofs modulo funextGravatar Jason Gross2018-12-19
* Move fancy rewrites after bounds analysisGravatar Jason Gross2018-12-12
* Add placeholder rewrite rules for rewriting after boundsGravatar Jason Gross2018-10-14
* Parameterize rewriter proofs over cast-outside-of-range behaviorGravatar Jason Gross2018-10-11
* Support type variables in patterns in the rewriterGravatar Jason Gross2018-09-29
* Finish rule-specific rewriter wf proofsGravatar Jason Gross2018-08-13
* Split up rewrite rules proofs into multiple filesGravatar Jason Gross2018-08-13
* Prove rewrite-rule-independent parts of rewrite WfGravatar Jason Gross2018-08-13
* Some WIP on Rewiter correctnessGravatar Jason Gross2018-07-30
* Integrate Wf and Interp proofsGravatar Jason Gross2018-07-30