Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
Also make those for introduction and elimination more symmetric: !% pure introduction % pure elimination !# always introduction # always elimination !> later introduction > pat timeless later elimination !==> view shift introduction ==> pat view shift elimination
Robbert Krebbers authoredAlso make those for introduction and elimination more symmetric: !% pure introduction % pure elimination !# always introduction # always elimination !> later introduction > pat timeless later elimination !==> view shift introduction ==> pat view shift elimination