GitLab

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.