Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
For example, when having `H : ▷ P → Q` and `HP : P`, we can now do `iSpecialize ("H" with "HP")`. This is achieved by putting a `FromAssumption` premise in the base instance for `IntoWand`.Robbert Krebbers authoredFor example, when having `H : ▷ P → Q` and `HP : P`, we can now do `iSpecialize ("H" with "HP")`. This is achieved by putting a `FromAssumption` premise in the base instance for `IntoWand`.
