Special proof mode class for adding a modality to a goal
This used to be done by using ElimModal
in backwards direction. Having
a separate type class for this gets rid of some hacks:
- Both
Hint Mode
s in forward and backwards direction forElimModal
. - Weird type class precedence hacks to make sure the right instance is picked.
These were needed because using
ElimModal
in backwards direction caused ambiguity.