Skip to content
Snippets Groups Projects
Select Git revision
  • adamAndMath/mfail
  • ci-release
  • ci/msammler/_1_2_lemmas
  • ci/msammler/more_feed
  • coq-stdpp-1.0
  • dfrumin/coq-stdpp-set_map_2
  • janno/tc-opaque-unseal
  • master default protected
  • msammler/bitvector
  • msammler/bool_decide_simpl_never
  • ralf/empty-opaque
  • ralf/hint-mode-check
  • ralf/hint-mode-plus
  • ralf/listZ
  • robbert/cbn
  • robbert/f_equiv_pointwise
  • robbert/from_option
  • robbert/map_filter_True_False
  • robbert/multiset_singleton
  • robbert/set_fold_union
  • coq-stdpp-1.8.0
  • coq-stdpp-1.7.0
  • coq-stdpp-1.6.0
  • coq-stdpp-1.5.0
  • coq-stdpp-1.4.0
  • coq-stdpp-1.3.0
  • coq-stdpp-1.2.1
  • coq-stdpp-1.2.0
  • coq-stdpp-1.1.0
  • coq-stdpp-1.0.0
30 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.028Jun27262524231918171615111098765432131May2827262520191817131176543230Apr292322212019151411831Mar2322191514131211524Feb181715121195129Jan28272320191715131187424Dec11109426Nov2320151211109231Oct30292821201513762129Sep161583231Aug3028724Jul2117161514102129Jun2523191817151429May282726191276130Apr292320171615111098765432131Mar302519181713109528Feb262524232019trailing newlineMerge branch 'changelog-addition' into 'master'Update changelog for filter extensionality lemmaschangelog for sum_inhabited_r fixMerge branch 'sum-inhabited-r' into 'master'Make sum_inhabited_r not a copy of sum_inhabited_lMerge branch 'ralf/insert_delete' into 'master'changelogrename insert_delete → insert_delete_insert; add new insert_delete matching delete_insertMerge branch 'extra-lemmas' into 'master'Add changelog entry and make small tweaksMerge branch 'robbert/pretty_N_go_stackoverflow' into 'master'Apply 1 suggestion(s) to 1 file(s)Merge branch 'ralf/fst_snd_map_zip' into 'master'Comment.Fix potential stack overflow related to `Pretty N`.add {fst,snd}_map_zipdeny warnings on 8.14 betatest Coq 8.14 beta branchAdd a few set and map related lemmasMerge branch 'robbert/cross_split' into 'master'CHANGELOG.Rewrite cross split lemmas so they can more easily be used for forward reasoning.Merge branch 'robbert/setoid' into 'master'Merge branch 'robbert/intersection_difference_filter' into 'master'CHANGELOG.Add lemmas `Permutation_equiv` and `equiv_Permutation`.Inversion lemmas for setoids on maps.Rename `equiv_None` → `None_equiv_eq`, add `Some_equiv_eq` to replace prior lemmas.Add lemmas `nil_equiv_eq`, `cons_equiv_eq`, `list_singleton_equiv_eq`, `app_equiv_eq`.`Proper`s for `union`, `union_with`, `intersection_with`, `difference_with` on `option`.Add lemma `map_filter_proper`.Add lemmas `map_intersection_filter` and `map_difference_filter`.Move setoid lemmas for maps to bottom of file.remove spurious spaceMerge branch 'robbert/relations_alt' into 'master'CHANGELOG.Add lemmas `rtc_nsteps_{1,2}` and `rtc_bsteps_{1,2}`.Prove more equivalences for closure operators on relations.Merge branch 'robbert/misc_map' into 'master'