Add various flavors of double delimiters

[Enivex]

Context: There are in essence four different types of double delimiters

1. "True" double delimiters, where the symbol is repeated twice

Based on naming conventions , these should get the .double modifier. I don't think this point is controversial.

2. A single delimiter closed with a vertical line (Comes from "Z-notation")

I called these .bar in the previous iteration, but used .closed here (following @MDLC01 's suggestion ). I'm not entirely happy with either name.

3. Black / filled delimiters.

There is only one pair of these, namely the tortoise shells ⦗ and ⦘. These don't show up correctly here, but here is what they look like in Noto Sans Math and Stix Two Math:

(They are completely broken in New Computer Modern Math)

The natural name is .filled

4. White / double-struck / stroked delimiters.

Currently we have a number of these introduced as .double, but this is not consistent with our typical naming. It also causes issues:

• There are actual doubled parentheses ⸨ and ⸩ in unicode (not compatibility characters!). While they are not mathematical delimiters, we may still want to add them to codex at some point, and paren.l.double / paren.r.double would be the natural names for them then.
• The tortoise shells above are the filled in variants of these:

which should therefore get the name .stroked. To quote @MDLC01 "If we have .stroked we should have it for everything that is not filled".

[knuesel]

These all make good sense to me. I don't find closed a bad name. The only alternative I can think of is chord but that seems needlessly technical.

[MDLC01]

To quote @MDLC01 "If we have .stroked we should have it for everything that is not filled".

I wrote that in a different context, as I clarified in #93 (comment).

Even though I don't like it, and I prefer .double, which is closer to what I would call those in English or French, I understand why .stroked makes sense, especially given the existence of ⸨ and ⸩.

Regarding the Z-notation characters, I don't think we have any for now (that are used only for Z-notation). I'm not sure how much sense it makes to add them. Is Z-notation still used? Do people using it need to write it inside documents? If so, won't they be copy-pasting it from somewhere else? We may want to defer the addition of characters that are only used in Z-notation until we figure that out.

[Enivex]

Regarding the Z-notation characters, I don't think we have any for now (that are used only for Z-notation). I'm not sure how much sense it makes to add them. Is Z-notation still used? Do people using it need to write it inside documents? If so, won't they be copy-pasting it from somewhere else? We may want to defer the addition of characters that are only used in Z-notation until we figure that out.

I wouldn't focus so much on the fact that the unicode name has Z-notation in them. As long as symbols are available, people will use them for other purposes as well. Most of the names introduced for this family of symbols in https://mirrors.mit.edu/CTAN/macros/unicodetex/latex/unicode-math/unimath-symbols.pdf have no reference to the fact that that's where they originated. (The exceptions being \zcmp, \zpipe and \zproject)

[MDLC01]

As long as symbols are available, people will use them for other purposes as well.

Well, that's what I'm unsure about. But if they indeed do then I'm completely fine with adding those symbols.