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

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

Do you want a CI run of all reverse deps with this branch?

Don't think that's needed, if there's fall out, I will fix.

But let's wait merging until Monday, I don't have time to fix other developments this weekend.

Is TCEq ever used where both sides are outputs? Otherwise we could also have two Hint Mode, i.e.

Hint Mode TCEq ! ! - : typeclass_instances.
Hint Mode TCEq ! - ! : typeclass_instances.

This way both directions would work, but the case where both sides are evars would be prevented. Also, it might make sense to both directions for TCForall2 as well, i.e. have

Hint Mode TCForall2 ! ! ! ! - : typeclass_instances.
Hint Mode TCForall2 ! ! ! - ! : typeclass_instances.

added 4 commits

• eded0f4c...f70ecc5c - 3 commits from branch master
• b130764f - Set `Hint Mode` for logical `TCX` type classes.

Compare with previous version

Excellent suggestion. Implemented that.

Merging.

mentioned in commit 20ef8941

merged