Skip to content

Special proof mode class for adding a modality to a goal

Robbert Krebbers requested to merge robbert/add_modal into master

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 Modes in forward and backwards direction for ElimModal.
  • Weird type class precedence hacks to make sure the right instance is picked. These were needed because using ElimModal in backwards direction caused ambiguity.

Merge request reports