Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 23
    • Merge requests 23
  • 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
  • IrisIris
  • Issues
  • #395
Closed
Open
Issue created Jan 04, 2021 by Simon Friis Vindum@simonfvContributor

Generalize frac to dfrac in view camera

The use of frac in the view camera could be generalized to dfrac. This would make it possible to "freeze" or persist the authorative element. I don't have a use case for this myself, but, if I recall correctly, @jung or @tchajed had one?

The notation would be the same as for the points-to predicate, and in the future the custom entries dfrac notation could be reused for this. The view camera is rather new, so breaking changes here are less critical, and it thus seems like a fine place to start with regards to trying to use dfrac more.

What do you think? I'd like to work on this if there is support.

Assignee
Assign to
Time tracking