Stream: Is there code for X?

Topic: how do I activate sum.lex?

Scott Morrison (Sep 10 2020 at 22:37):

Are there some defs somewhere that I can local attribute [instance] to turn on sum.lex as a preorder/partial_order/...?

Scott Morrison (Sep 10 2020 at 22:38):

(i.e. assuming the corresponding structure on both sides of the sum?)

Yury G. Kudryashov (Sep 14 2020 at 08:57):

It seems that sum.lex takes two relations as arguments. I can't find any lemmas about sum.lex being preorder etc

Last updated: May 17 2021 at 15:13 UTC