GitLab

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.