-
Dan Frumin authored
- The typeclass `PureExec e1 e2` controls pure deterministic reductions - General tactics rel_pure_l and rel_pure_r that depend on that typeclass - The same typeclass can be used for WP tactics and tp tactics, potentially
d7cada37