Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 174
    • Issues 174
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 20
    • Merge requests 20
  • 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
  • #412
Closed
Open
Issue created Apr 19, 2021 by Ralf Jung@jungOwner

Use dfrac everywhere

auth and view support dfrac now, but many of the abstractions built on top of it do not yet:

  • algebra.lib.gmap_view
  • algebra.lib.mono_nat
  • base_logic.lib.ghost_map
  • base_logic.lib.mono_nat

There are more auth-based abstractions in algebra.lib but those do not expose any fraction on their authoritative part yet.

Some more are not actually built on top of view, but these are or could be exposing fractions that it might be useful to turn into dfrac:

  • base_logic.lib.ghost_var
  • Cancelable invariants
  • Saved propositions (could be made essentially "ghost_var with higher-order ghost state", supporting both persistent immutable and ephemeral mutable saved propositions)

However, before we do all this, we should figure out if there is a way to do that without making these APIs harder to use for the common case of only needing fraction 1. For gset_bij, we are already in the situation that users need to write DfracOwn 1 a lot; I wouldn't want the same to happen e.g. for ghost_map.

Edited Jan 17, 2022 by Ralf Jung
Assignee
Assign to
Time tracking