aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments
Commit message (Expand)AuthorAge
* move weight proofs up above Positional so they can be used to prove eval_drop...Gravatar jadep2018-12-21
* modify a proof because in 8.7 [auto] doesn't solve the goalGravatar jadep2018-12-21
* prove admitGravatar jadep2018-12-21
* prove admitGravatar jadep2018-12-21
* Add Wf_reifyGravatar Jason Gross2018-12-20
* Add Wf_APP, Interp_reifyGravatar Jason Gross2018-12-20
* Remove glue admits in Toplevel1Gravatar Jason Gross2018-12-20
* Add uweight_partition_unique, move weight_1 to uweight_1, add Positional.eval...Gravatar Jason Gross2018-12-20
* Finish rewriter proofs modulo funextGravatar Jason Gross2018-12-19
* Add eq_subst_types_pattern_collect_vars_empty_iffGravatar Jason Gross2018-12-18
* Add rawexpr_types_okGravatar Jason Gross2018-12-14
* Fix an issue with setoid_rewrite being weaker before 8.9Gravatar Jason Gross2018-12-14
* Add reify_and_let_binds_base_interp_relatedGravatar Jason Gross2018-12-14
* add interp_related_gen_of_wfGravatar Jason Gross2018-12-12
* 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
* Fix a bug in 0672c92921e45b942fa8a75c45457b8c7b32565dGravatar Jason Gross2018-12-12
* Add type.eq_subst_types_pattern_collect_varsGravatar Jason Gross2018-12-12
* Make unify_pattern' a bit stricterGravatar 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 01:46:37 +0000