HOL Unicode for BIGINTER, BIGUNION

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

Oct 22 '12 13:10 xrchz

Do you have any suggested code-points?

Oct 22 '12 23:10 mn200

U+22C2 and U+22C3, or U+2229 and U+222A seem like good candidates.

http://www.fileformat.info/info/unicode/char/22c2/index.htm http://www.fileformat.info/info/unicode/char/22c3/index.htm http://www.fileformat.info/info/unicode/char/2229/index.htm http://www.fileformat.info/info/unicode/char/222a/index.htm

Oct 31 '12 08:10 xrchz

Go ahead. I guess the issue is whether or not the “n-ary” symbols (U+22C2 and U+22C3) are different enough from the other two, particularly in the fonts we’re likely to be using.

It might also be worth thinking about having BIGUNION_IMAGE so that we can write things like

\bigcup_{x\in S} f(x)

(BIGUNION (IMAGE f S) occurs a lot in our sources already.) BIGUNION would then be BIGUNION_IMAGE I (by analogy with SUM_IMAGE and SUM_SET). Perhaps the derived ones should just be abbreviations rather than definitions too...

See also #51 for more on the pretty-printing/parsing side of things here.

Nov 01 '12 00:11 mn200