Draft: Add simple library for priority levels and use it for `iFrame`
As already discussed here: !739 (merged)
I now designed a solution that does not require to add an additional argument to the Frame
class. Instead, it puts a dummy constant in the Coq context, and rules that have side-conditions on the priority level have a TC premise that checks if the level is OK. I have implemented the priority levels as a separate library that in principle could be used for other tactics too.
TODO:
- Figure out where the priority level library should go to. I put it in
iris.proofmode
, but in principle it has nothing to with the proof mode. - Figure out syntax for
iFrame
and friends to give the priority level in a concise way. - Determine what levels we need for
iFrame
. I think we don't want framing for ∧, ∨, and Fractional by default. Are there more examples? What levels would be appropriate? - Adapt the proof scripts, I currently use
at_level
by lack of syntax.
Edited by Robbert Krebbers