aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments
Commit message (Expand)AuthorAge
* remove pattern.ident.type_varsGravatar Jason Gross2018-12-11
* Use Fixpoint, not list_rect, for {app,lam}_forall_varsGravatar Jason Gross2018-12-11
* Add eqv_iff_eq_of_funextGravatar 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
* Yet more repeat fixingGravatar Jason Gross2018-12-04
* 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
* Fix bug in previous commitGravatar Jason Gross2018-11-16
* 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 UnderLets.wf_interp_ProperGravatar Jason Gross2018-11-15
* Add a couple of useful lemmasGravatar Jason Gross2018-11-15
* Uncurry rewriter rulesGravatar Jason Gross2018-11-15
* Base Dead Code Elim on Subst01Gravatar Jason Gross2018-11-15
* Add support for parsing Q and boolGravatar Jason Gross2018-11-12
* 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
* Revert "Disable very very slow printing"Gravatar Jason Gross2018-11-07
* Fix the s-adjustment for saturated solinasGravatar Jason Gross2018-11-06
* Disable very very slow printingGravatar Jason Gross2018-11-06
* Revert "Factor out a common computation to fix n² behavior"Gravatar Jason Gross2018-11-06
* Factor out a common computation to fix n² behaviorGravatar Jason Gross2018-11-06
* Use a better strategy in Rows.sat_reduceGravatar Jason Gross2018-11-06
* Restrict [ident.cast] a bit moreGravatar Jason Gross2018-11-05
* Add .out files for rewriterGravatar Jason Gross2018-11-02
* Also inline Z_cast thingsGravatar Jason Gross2018-11-01
* Make pairs work in Z_cast2Gravatar Jason Gross2018-11-01
* Fix a thing broken by previous commitGravatar Jason Gross2018-11-01
* Remove dead codeGravatar Jason Gross2018-11-01
* Fix a bug in 8.7 compilationGravatar Jason Gross2018-10-30
* Refactor/generalize some pipeline definitions/proofsGravatar Jason Gross2018-10-30
* Remove duplicate abstractionGravatar Jasper Hugunin2018-10-29
* Stricter check on types in the rewriterGravatar Jason Gross2018-10-29
* 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
* Add an extra check in the rewriterGravatar 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 19:06:07 +0000