Skip to content
GitLab
  • Menu
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 69
    • Issues 69
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 6
    • Merge requests 6
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !176

Remove `map` infix in lemmas about `dom` and `filter`.

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/dom_filter into master Jul 16, 2020
  • Overview 1
  • Commits 1
  • Changes 2

The combination of dom and filter only makes sense for maps, so the map infix is useless. Other similar lemmas do not have such an infix either, so it's also inconsistent.

Rename dom_map filter → dom_filter, dom_map_filter_L → dom_filter_L, and dom_map_filter_subseteq → dom_filter_subseteq.

This was pointed out by @atrieu in !175 (comment 53746)

Edited Jul 16, 2020 by Robbert Krebbers
Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: robbert/dom_filter