• Robbert Krebbers's avatar
    Generalize update tactics into iMod and iModIntro for modalities. · fc30ca08
    Robbert Krebbers authored
    There are now two proof mode tactics for dealing with modalities:
    
    - `iModIntro` : introduction of a modality
    - `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality
    
    The behavior of these tactics can be controlled by instances of the `IntroModal`
    and `ElimModal` type class. We have declared instances for later, except 0,
    basic updates and fancy updates. The tactic `iMod` is flexible enough that it
    can also eliminate an updates around a weakest pre, and so forth.
    
    The corresponding introduction patterns of these tactics are `!>` and `>`.
    
    These tactics replace the tactics `iUpdIntro`, `iUpd` and `iTimeless`.
    
    Source of backwards incompatability: the introduction pattern `!>` is used for
    introduction of arbitrary modalities. It used to introduce laters by stripping
    of a later of each hypotheses.
    fc30ca08
ProofMode.md 11.1 KB