Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 122
    • Issues 122
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 18
    • Merge Requests 18
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Iris
  • Iris
  • Merge Requests
  • !403

Merged
Opened Mar 27, 2020 by Ralf Jung@jungOwner

make names of more `f_op`/`f_core` rewrite lemmas more consistent

  • Overview 71
  • Commits 4
  • Changes 9

The _op etc should be a suffix.

What this MR does not fix is the inconsistency between the f_op lemmas on the one side and the f_core/f_included lemmas on the other side: the former have the "operation at the result type of f" (so, e.g. the composition of gmaps, for the singleton_ lemmas) on the right-hand side, while the latter have it on the left-hand side.

Cc @iris-users because this is a breaking change, but should be fairly easy to fix.

Edited Apr 06, 2020 by Ralf Jung
Assignee
Assign to
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Reference: iris/iris!403
Source branch: ralf/rename_op_core

Revert this merge request

This will create a new commit in order to revert the existing changes.

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.

Cherry-pick this merge request

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.