aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
Commit message (Expand)AuthorAge
* Uncurry rewriter rulesGravatar Jason Gross2018-11-15
* Update the post-bounds rewrite rulesGravatar Jason Gross2018-11-11
* Split off all of the arithmetic rules that need bounds infoGravatar Jason Gross2018-11-11
* Add under_forall_vars_relation1_lam_forall_vars, remove forall2_type_of_list_...Gravatar Jason Gross2018-10-25
* Update rewriter correctness conditionGravatar Jason Gross2018-10-23
* 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
* Add interp-correctness condition for rewriterGravatar Jason Gross2018-10-11