solver for orders?

Stream: new members

[Joachim Breitner]

Is there a tactic that solves obligations that hold in any partial order? (not urgent, I'm just curious)

[Kevin Buzzard]

library_search ;-) Are you seeing complex obligations? Maybe linarith will do them in some situations (i.e when your partial order is actually the real numbers) but I don't think it works for general partial orders.

[Yaël Dillies]

ask_yael :grinning:

[Kevin Buzzard]

It might be a fun tactic to write : e.g. a <= b and b <= c and c <= a implies a = b