aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists
AgeCommit message (Expand)Author
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-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
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-05-23Fixing typos - Part 3JPR
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
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-04-16Protecting against a "deprecated cofix" warning.Hugo Herbelin
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-15Make list functions returning sumbools transparentTej Chajed
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 22:09:32 +0000