Zulip Chat Archive

Stream: Is there code for X?

Topic: how do I activate `sum.lex`?


view this post on Zulip 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/...?

view this post on Zulip Scott Morrison (Sep 10 2020 at 22:38):

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

view this post on Zulip 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