Skip to content
Snippets Groups Projects
Select Git revision
  • ci-release protected
  • ci/msammler/more_feed
  • ci/refactor_staging
  • coq-stdpp-1.0 protected
  • dfrumin/coq-stdpp-set_map_2
  • master default protected
  • msammler/bitvector
  • msammler/bool_decide_simpl_never
  • msammler/monad_without_universe_constraints
  • ralf/empty-opaque
  • ralf/hint-mode-check
  • ralf/hint-mode-plus
  • ralf/listZ
  • ralf/lookup_insert
  • ralf/make_simple_intropattern
  • ralf/multiset-solver
  • ralf/no-notypeclasses-apply
  • robbert/cancel_inj_surj
  • robbert/cbn
  • robbert/f_equiv_pointwise
  • coq-stdpp-1.11.0 protected
  • coq-stdpp-1.10.0 protected
  • coq-stdpp-1.9.0 protected
  • coq-stdpp-1.8.0 protected
  • coq-stdpp-1.7.0 protected
  • coq-stdpp-1.6.0 protected
  • coq-stdpp-1.5.0 protected
  • coq-stdpp-1.4.0 protected
  • coq-stdpp-1.3.0 protected
  • coq-stdpp-1.2.1 protected
  • coq-stdpp-1.2.0 protected
  • coq-stdpp-1.1.0 protected
  • coq-stdpp-1.0.0 protected
33 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.024Jun231918171615111098765432131May2827262520191817131176543230Apr292322212019151411831Mar2322191514131211524Feb181715121195129Jan28272320191715131187424Dec11109426Nov2320151211109231Oct30292821201513762129Sep161583231Aug3028724Jul2117161514102129Jun2523191817151429May282726191276130Apr292320171615111098765432131Mar302519181713109528Feb26252423201918171413Apply 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'Add lemmas `merge_empty_l` and `merge_empty_r`.Add lemma `map_filter_lookup`.Add lemma `map_fmap_singleton_inv`.Merge branch 'robbert/head_tail' into 'master'Add tests for `simpl` on `last`.Comment about `head` and `tail` notations.CHANGELOG.Add lemmas for `head` similar to those for `tail`.Define `head` as notation that also prints (Coq defines it as `parsing only`).More properties of `last` function.Make sure `tail` is not `simpl`ed too much.Merge branch 'robbert/lookup_merge' into 'master'