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
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
Last updated: May 17 2021 at 15:13 UTC