Skip to content
Snippets Groups Projects

Add some _1, _2 lemmas for map_filter

Merged Michael Sammler requested to merge ci/msammler/_1_2_lemmas into master

As discussed with @robbertkrebbers

Edited by Ralf Jung

Merge request reports

Merge request pipeline #115705 passed

Merge request pipeline passed for 5a5578b4

Merged by Robbert KrebbersRobbert Krebbers 2 weeks ago (Feb 5, 2025 5:49pm UTC)

Merge details

  • Changes merged into with 96ef0cd6.
  • Deleted the source branch.

Pipeline #115734 passed

Pipeline passed for 96ef0cd6 on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
    • Resolved by Ralf Jung

      I think the not_elem_of_dom and lookup_union_None lemmas are no-brainers and could be added asap.

      The filter lemmas are a bit more of a headache since we need to make sure they are consistent with those for set/list.

      Could you maybe split up the MR?

      Edited by Robbert Krebbers
  • Michael Sammler added 30 commits

    added 30 commits

    Compare with previous version

  • Michael Sammler mentioned in merge request !405 (merged)

    mentioned in merge request !405 (merged)

  • added 1 commit

    Compare with previous version

  • Ralf Jung changed title from Add some _1, _2 lemmas to Add some _1, _2 lemmas for map_filter

    changed title from Add some _1, _2 lemmas to Add some _1, _2 lemmas for map_filter

  • Status: needs figuring out the names for the new lemmas and making sure they are consistent with sets and lists. @robbertkrebbers says he has some half-finished work somewhere he'll try to dig out.

  • Ralf Jung
  • Ralf Jung mentioned in merge request !582 (merged)

    mentioned in merge request !582 (merged)

  • Michael Sammler added 537 commits

    added 537 commits

    Compare with previous version

  • Michael Sammler added 123 commits

    added 123 commits

    Compare with previous version

  • added 1 commit

    • ce64df0e - Add _1, _2 lemmas for map_empty_filter

    Compare with previous version

  • added 1 commit

    • ba934995 - Add _1, _2 lemmas for map_empty_filter

    Compare with previous version

  • Ralf Jung resolved all threads

    resolved all threads

  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Please register or sign in to reply
    Loading