Capital letters

Stream: new members

[Iocta]

What is the convention for capitalization, like Union vs union?

[Mario Carneiro]

Almost everything is in all lowercase snake_case, but there are a few exceptions for name segments with particular meanings. There are a few related union-like functions, which have names differ in capitalization:

• union : set A -> set A -> set A means the binary union of two sets (or finsets, etc)
• Union : (I -> set A) -> set A is the indexed union of a family of sets
• sUnion : set (set A) -> set A is the union of a set of sets
• bUnion is the name for the iterated union U i \in s, f i, essentially having the type set I -> (I -> set A) -> set A
  There is a similar pattern with inter, Inter, sInter and bInter.

Another capitalized name segment, for similar reasons, is the same sequence of functions, this time for lattices:

• sup, inf: binary supremum/infimum
• supr, infi: supremum/infimum over a type
• Sup, Inf: supremum/infimum over a set of elements
• bSup, bInf: bounded supremum/infimum

[Scott Morrison]

We also use Group for a bundled group, etc.

[Bryan Gin-ge Chen]

Anyone want to add this to our naming conventions doc here?