• 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
Name
Last commit
Last update
..
lib Loading commit data...
adequacy.v Loading commit data...
derived.v Loading commit data...
heap.v Loading commit data...
lang.v Loading commit data...
lifting.v Loading commit data...
notation.v Loading commit data...
proofmode.v Loading commit data...
tactics.v Loading commit data...
wp_tactics.v Loading commit data...