Skip to content

Set `Hint Mode` for logical `TCX` type classes

Robbert Krebbers requested to merge robbert/TCX_hint_mode into master

This closes issue #55 (closed).

Note that both arguments of TCEq are outputs, which makes TCEq symmetric. We could make one the input argument and the other the output argument, but this requires some change to Iris without obvious benefits.

/cc @msammler @janno

Merge request reports