Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
It now traverses terms at most once, whereas the setoid_rewrite approach was travering terms many times. Also, the tactic can now be extended by defining type class instances.
Robbert Krebbers authoredIt now traverses terms at most once, whereas the setoid_rewrite approach was travering terms many times. Also, the tactic can now be extended by defining type class instances.