[ new ] unicode symbols for various 'tacks' (#7791)

* [ new ] unicode symbols for various 'tacks'

We discussed using the bbot in agda/agda-stdlib#2595

* Fix silly mistake

* [ changelog ] for the emacs mode extension

Author: gallais

CHANGELOG.md

@@ -283,6 +283,7 @@ Interaction and emacs mode
   This is only a surface-level fix, since Agda might still fail to find the properly qualified name for
   the constructor in scope, but should at least make more sense in most situations.
 
+* New bindings for unicode 'tacks' (⟘⟙⟛⟝⟞⫫⫪) via \tack (as well as specialised names for each of them)
 
 Backends
 --------

src/data/emacs-mode/agda-input.el

@@ -256,7 +256,7 @@ order for the change to take effect."
   ("glb" . ("⊓"))  ("lub" . ("⊔"))
   ("Glb" . ("⨅"))  ("Lub" . ("⨆"))
 
-  ;; Entailment etc.
+  ;; Entailment, tacks, etc.
 
   ("entails" . ,(agda-input-to-string-list "⊢⊣⊤⊥⊦⊧⊨⊩⊪⊫⊬⊭⊮⊯"))
 
@@ -267,6 +267,16 @@ order for the change to take effect."
   ("||="  . ("⊫"))  ("||=n" . ("⊯"))
   ("|||-" . ("⊪"))
 
+
+  ("tack" . ,(agda-input-to-string-list "⟘⟙⟛⟝⟞⫫⫪"))
+  ("Bot"  . ("⟘")) ;; similar to Glb/Lub vs. glb/lub
+  ("Top"  . ("⟙"))
+  ("-||-" . ("⟛"))
+  ("|--"  . ("⟝"))
+  ("--|"  . ("⟞"))
+  ("bbot" . ("⫫")) ;; similar to bN for blackboard N
+  ("btop" . ("⫪"))
+
   ;; Divisibility, parallelity.
 
   ("|"  . ("∣"))  ("|n"  . ("∤"))