Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 84
    • Issues 84
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 9
    • Merge requests 9
  • 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
  • !444

Add images (codomains) to finite maps

  • Review changes

  • Download
  • Patches
  • Plain diff
Merged Dorian Lesbre requested to merge dlesbre/stdpp:dorian/fin-map-img into master Feb 09, 2023
  • Overview 40
  • Commits 24
  • Pipelines 20
  • Changes 3

Simple axiomatization of finite map images (also called codomains). This is strongly inspired by the implementation of dom.

It doesn't contain nearly as much lemmas though, mainly because results on the image are generally much weaker than those on the domain, so just using the definition seems simple then providing overly complex lemmas.

Disclaimers: I'm not exactly an expert in Coq but eager to learn more. If you find that my coding style and proofs are ugly, inefficient, impractical or not in keeping with recommended guidelines feel free to let me know.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: dorian/fin-map-img