["\\smile" ], "⌣", [symbol];
["\\blank" ], "␣", [symbol];
["\\HorizontalLine" ], "─", [symbol];
- ["\\loz"; "\\lozenge" ], "◊", [symbol];
+ ["\\loz"; "\\lozenge";"<>" ], "◊", [symbol];
["\\starf"; "\\bigstar" ], "★", [symbol];
["\\phone" ], "☎", [symbol];
["\\female" ], "♀", [symbol];
["\\wedgeq" ], "≙", [equivalence];
["\\veeeq" ], "≚", [equivalence];
["\\trie"; "\\triangleq" ], "≜", [equivalence];
- ["\\def" ], "≝", [equivalence];
+ ["\\def";":=" ], "≝", [equivalence];
["\\equest"; "\\questeq" ], "≟", [equivalence];
["\\ne"; "\\neq"; "\\NotEqual" ], "≠", [equivalence];
["\\equiv"; "\\Congruent" ], "≡", [equivalence];
["\\NotNestedLessLess" ], "⒡̸", [circle];
["\\NotNestedGreaterGreater" ], "⒢̸", [circle];
["\\oS"; "\\circledS" ], "Ⓢ", [circle];
- ["\\cir" ], "○", [circle];
+ ["\\cir"; ], "○", [circle];
["\\xcirc"; "\\bigcirc" ], "◯", [circle];
(* }}} *)
["\\sdotb"; "\\dotsquare" ], "⊡", [square];
["\\uhblk" ], "▀", [square];
["\\lhblk" ], "▄", [square];
- ["\\squ"; "\\square"; "\\Square" ], "□", [square];
+ ["\\squ"; "\\square"; "\\Square";"[]" ], "□", [square];
["\\squf"; "\\squarf"; "\\blacksquare" ], "▪", [square];
["\\rect" ], "▭", [square];
["\\marker" ], "▮", [square];
;;
let predefined_classes = [
- [ "→"; "⇉"; "⇒"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; "⥤"; "⥰"; ] ;
- [ "≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; ];
- [ "_" ; "⎽"; "⎼"; "⎻"; "⎺"; ];
- [ "<"; "≺"; "≮"; "⊀"; ] ;
+ ["→"; "⇉"; "⇒"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; "⥤"; "⥰"; ] ;
+ ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; ];
+ ["_" ; "⎽"; "⎼"; "⎻"; "⎺"; ];
+ ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; ] ;
+ ["□"; "◽"; "▪"; "◾"; ];
+ ["◊"; "♢"; "⧫"; "♦"; ];
+ [">"; "〉"; "»"; ];
["a"; "α"; "𝕒"; ] ;
["A"; "ℵ"; "𝔸"; ] ;
["b"; "β"; "ß"; "𝕓"; ] ;
["M"; "ℳ"; "𝕄"; ] ;
["n"; "𝕟"; ] ;
["N"; "ℕ"; "№"; ] ;
- ["o"; "θ"; "ϑ"; "𝕠"; "ø"; "∘"; ] ;
+ ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "ø"; "○"; ] ;
["O"; "Θ"; "𝕆"; ] ;
["p"; "π"; "𝕡"; ] ;
["P"; "Π"; "℘"; "ℙ"; ] ;
["Y"; "ϒ"; "𝕐"; ] ;
["z"; "ζ"; "𝕫"; ] ;
["Z"; "ℨ"; "ℤ"; ] ;
+ ["0"; "𝟘"; ] ;
+ ["1"; "𝟙"; ] ;
+ ["2"; "𝟚"; ] ;
+ ["3"; "𝟛"; ] ;
+ ["4"; "𝟜"; ] ;
+ ["5"; "𝟝"; ] ;
+ ["6"; "𝟞"; ] ;
+ ["7"; "𝟟"; ] ;
+ ["8"; "𝟠"; ] ;
+ ["9"; "𝟡"; ] ;
]
;;