aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists/List.v
AgeCommit message (Expand)Author
2021-03-26remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, SetoidAndrej Dudenhefner
2021-03-23add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, Forall_map,...Andrej Dudenhefner
2021-01-29add results on count_occOlivier Laurent
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-09-16Modify Lists/List.v to compile with -mangle-namesJasper Hugunin
2020-09-07Add iff variants for other list lemmasEdward Wang
2020-09-07Add iff variant for app_inj_tailEdward Wang
2020-08-12Additional statements about List.repeatOlivier Laurent
2020-05-09Merge PR #12237: [stdlib] [List] add results around incl, filter and nthHugo Herbelin
2020-05-04add incl_Forall_in_iffOlivier Laurent
2020-05-04strenghten nth_extOlivier Laurent
2020-05-04add incl_map incl_filter NoDup_filterOlivier Laurent
2020-04-30Symmetry in conclusions of List.map_eq_*Olivier Laurent
2020-04-19remove useless hypothesis in NoDup_Permutation_bisOlivier Laurent
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-17Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]Hugo Herbelin
2020-01-06stdlib List: add [remove'] and [count_occ']Yishuai Li
2020-01-05apply suggestions of @anton-trunovOlivier Laurent
2020-01-05clean some indentationsOlivier Laurent
2019-12-06additional statements on flat_mapOlivier Laurent
2019-12-06additional statements on map and ForallOlivier Laurent
2019-12-06integration of statements for nthOlivier Laurent
2019-12-06add elt_eq_unitOlivier Laurent
2019-12-06integration of statements for Exists and ForallOlivier Laurent
2019-12-06integration of list_sum and list_maxOlivier Laurent
2019-12-06integration of statements for repeatOlivier Laurent
2019-12-06integration of statements for NoDupOlivier Laurent
2019-12-06integration of additional statements for inclOlivier Laurent
2019-12-06integration of statements for removeOlivier Laurent
2019-12-06integration of statements for InOlivier Laurent
2019-12-06integration of statements for inclOlivier Laurent
2019-12-06integration of statements for revOlivier Laurent
2019-12-06integration of statements for concat and flat_mapOlivier Laurent
2019-12-06integration of statements for seqOlivier Laurent
2019-12-06integration of statements related to last elementOlivier Laurent
2019-12-06integration of Exists_or and Forall_andOlivier Laurent
2019-12-06redundancy between skipn_node and skipn_allOlivier Laurent
2019-09-03Add lemmas directly relating List.nth and List.nth_errorOliver Nash
2019-09-03Remove redundant parameter in List.concat_filter_mapOliver Nash
2019-09-03New lemmas for List.vOliver Nash
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2018-11-27Added two proofs to the Lists library. The first, Forall_inv_tail, extends Fo...llee454@gmail.com
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-09-29New lemmas for List.vSimon Marechal
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:11:53 +0000