aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/RewriterWf1.v
Commit message (Expand)AuthorAge
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
* Add eq_subst_types_pattern_collect_vars_empty_iffGravatar Jason Gross2018-12-18
* Add rawexpr_types_okGravatar Jason Gross2018-12-14
* Generalize expr.interp_relatedGravatar Jason Gross2018-12-12
* Add type.eq_subst_types_pattern_collect_varsGravatar Jason Gross2018-12-12
* Add projT1_app_with_unification_resultTGravatar Jason Gross2018-12-12
* Add rawexpr_interp_related_Proper_rawexpr_equiv_rew_genGravatar 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
* Prove pattern.ident.type_vars_enoughGravatar Jason Gross2018-12-08
* Add value_of_rawexpr_interp_relatedGravatar Jason Gross2018-12-07
* Switch to a more precise version of interp_related for rewritesGravatar Jason Gross2018-12-07
* Add value_or_expr_interp_okGravatar Jason Gross2018-11-29
* Add unfold_value'_interp_arrowGravatar Jason Gross2018-11-28
* Add value_interp_ok_{arrow,base}Gravatar Jason Gross2018-11-28
* Add some more rawexpr equiv lemmasGravatar Jason Gross2018-11-27
* Add reveal_rawexpr_equivGravatar Jason Gross2018-11-27
* Restrict rawexpr_equiv to match with reveal betterGravatar Jason Gross2018-11-27
* Add value_interp_self_related_of_okGravatar Jason Gross2018-11-27
* Add some lemmas about substGravatar Jason Gross2018-11-27
* Refactor interpretation of valuesGravatar Jason Gross2018-11-27
* Add related_sigT_by_eqGravatar Jason Gross2018-11-16
* Add app_forall_vars_lam_forall_varsGravatar Jason Gross2018-11-16
* Add some lemmas about wf value interp relatedGravatar Jason Gross2018-11-15
* Add a couple of useful lemmasGravatar Jason Gross2018-11-15
* Uncurry rewriter rulesGravatar Jason Gross2018-11-15
* Add subst_relaxGravatar Jason Gross2018-10-29
* Add subst_Some_subst_default, subst_relax_evmGravatar Jason Gross2018-10-29
* Fix a proofGravatar Jason Gross2018-10-28
* Improve cps_id tactics, add add_var_types_cps_id, unify_extracted_cps_id tacticsGravatar Jason Gross2018-10-28
* Add unify_extracted_cps_idGravatar Jason Gross2018-10-28
* Add app_lam_type_of_listGravatar Jason Gross2018-10-25
* Add under_forall_vars_relation1_lam_forall_vars, remove forall2_type_of_list_...Gravatar Jason Gross2018-10-25
* Remove value'_interp_related1Gravatar Jason Gross2018-10-25
* Add value_interp_related1Gravatar Jason Gross2018-10-25
* Add rawexpr_equiv_expr_to_type_of_rawexprGravatar Jason Gross2018-10-23
* Add a horribly manual proof of app_forall_vars_under_forall_vars_relation1Gravatar Jason Gross2018-10-23
* Add under_with_unification_resultT'_relation1_gen_alwaysGravatar Jason Gross2018-10-23
* Add related1_app_type_of_list_under_type_of_list_relation1_cpsGravatar Jason Gross2018-10-23
* Update rewriter correctness conditionGravatar Jason Gross2018-10-23
* Minor changes to rewriterGravatar Jason Gross2018-10-14
* Add interp-correctness condition for rewriterGravatar 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
* Improvements in rewrite-rule-specific proofsGravatar Jason Gross2018-08-13
* Split up rewrite rules proofs into multiple filesGravatar Jason Gross2018-08-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 23:54:27 +0000