diff options
| author | Matthias Georg Mayer <Matthias.Georg.Mayer@Gmail.com> | 2023-05-30 18:05:24 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-05-30 18:05:24 +0200 |
| commit | 789a54f9e5fcebf4a3b3945d36ce3db7674b0fbc (patch) | |
| tree | 3bd6ce1ace68c28c9f35630cce955940dfd8ba6b /library | |
| parent | 7e07b61046ec43369fb8f2e281b71c4e5988f5fc (diff) | |
Add ⊬ to symbols.rs (#1318)
Diffstat (limited to 'library')
| -rw-r--r-- | library/src/symbols/sym.rs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/library/src/symbols/sym.rs b/library/src/symbols/sym.rs index 410eff4f..a871d29f 100644 --- a/library/src/symbols/sym.rs +++ b/library/src/symbols/sym.rs @@ -718,7 +718,9 @@ pub(crate) const SYM: &[(&str, Symbol)] = symbols! { ], tack: [ r: '⊢', + r.not: '⊬', r.long: '⟝', + r.short: '⊦', r.double: '⊨', r.double.not: '⊭', l: '⊣', |