aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
Commit message (Expand)AuthorAge
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
* Finish proving fancy rewrite rulesGravatar Jason Gross2019-01-03
* try to fix fancy rewrite rules; current output is incorrectGravatar jadep2019-01-03
* Remove useless assumptionsGravatar Jason Gross2018-12-12
* Generalize expr.interp_relatedGravatar Jason Gross2018-12-12
* Move fancy rewrites after bounds analysisGravatar Jason Gross2018-12-12
* remove pattern.ident.type_varsGravatar Jason Gross2018-12-11
* Use Fixpoint, not list_rect, for {app,lam}_forall_varsGravatar Jason Gross2018-12-11
* Switch to a more precise version of interp_related for rewritesGravatar Jason Gross2018-12-07
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 05:18:08 +0000