From d4a929febb0c51f1fddf48eb83ba1de0b4cc56f9 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 17 Apr 2015 13:15:16 -0400
Subject: [PATCH] feat(lean-input): add some notation

---
 src/emacs/lean-input.el | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el
index 686883cff..dd56b11d7 100644
--- a/src/emacs/lean-input.el
+++ b/src/emacs/lean-input.el
@@ -202,15 +202,17 @@ order for the change to take effect."
 
   ("eq"  . ,(lean-input-to-string-list "=∼∽≈≋∻∾∿≀≃⋍≂≅ ≌≊≡≣≐≑≒≓≔≕≖≗≘≙≚≛≜≝≞≟≍≎≏≬⋕"))
   ("eqn" . ,(lean-input-to-string-list "≠≁ ≉     ≄  ≇≆  ≢                 ≭    "))
+  ("equiv" . ,(lean-input-to-string-list "≃⋍"))
+  ("iso" . ,(lean-input-to-string-list "≅≌"))
 
                     ("=n"  . ("≠"))
   ("~"    . ("∼"))  ("~n"  . ("≁")) ("homotopy"    . ("∼"))
   ("~~"   . ("≈"))  ("~~n" . ("≉"))
   ("~~~"  . ("≋"))
   (":~"   . ("∻"))
-  ("~-"   . ("≃"))  ("~-n" . ("≄")) ("equiv"   . ("≃"))
+  ("~-"   . ("≃"))  ("~-n" . ("≄"))
   ("-~"   . ("≂"))
-  ("~="   . ("≅"))  ("~=n" . ("≇")) ("iso"   . ("≅"))
+  ("~="   . ("≅"))  ("~=n" . ("≇"))
   ("~~-"  . ("≊"))
   ("=="   . ("≡"))  ("==n" . ("≢"))
   ("==="  . ("≣"))
@@ -238,10 +240,10 @@ order for the change to take effect."
 
   ;; Inequality and similar symbols.
 
-  ("leq"  . ,(lean-input-to-string-list "<≪⋘≤≦≲ ≶≺≼≾⊂⊆ ⋐⊏⊑ ⊰⊲⊴⋖⋚⋜⋞"))
-  ("leqn" . ,(lean-input-to-string-list "≮  ≰≨≴⋦≸⊀ ⋨⊄⊈⊊  ⋢⋤ ⋪⋬   ⋠"))
-  ("geq"  . ,(lean-input-to-string-list ">≫⋙≥≧≳ ≷≻≽≿⊃⊇ ⋑⊐⊒ ⊱⊳⊵⋗⋛⋝⋟"))
-  ("geqn" . ,(lean-input-to-string-list "≯  ≱≩≵⋧≹⊁ ⋩⊅⊉⊋  ⋣⋥ ⋫⋭   ⋡"))
+  ("leq"  . ,(lean-input-to-string-list "≤≦≲<≪⋘ ≶≺≼≾⊂⊆ ⋐⊏⊑ ⊰⊲⊴⋖⋚⋜⋞"))
+  ("leqn" . ,(lean-input-to-string-list "≰≨≮≴⋦   ≸⊀ ⋨⊄⊈⊊  ⋢⋤ ⋪⋬   ⋠"))
+  ("geq"  . ,(lean-input-to-string-list "≥≧≳>≫⋙ ≷≻≽≿⊃⊇ ⋑⊐⊒ ⊱⊳⊵⋗⋛⋝⋟"))
+  ("geqn" . ,(lean-input-to-string-list "≱≩≯≵⋧ ≹  ⊁ ⋩⊅⊉⊋  ⋣⋥ ⋫⋭   ⋡"))
 
   ("<="   . ("≤"))  (">="   . ("≥"))
   ("<=n"  . ("≰"))  (">=n"  . ("≱"))
@@ -322,6 +324,8 @@ order for the change to take effect."
 
   ;; Various operators/symbols.
   ("tr"        . ,(lean-input-to-string-list "⬝▹"))
+  ("trans"     . ,(lean-input-to-string-list "▹⬝"))
+  ("transport" . ("▹"))
   ("con"       . ("⬝"))
   ("cdot"      . ("⬝"))
   ("sy"        . ("⁻¹"))
@@ -451,9 +455,8 @@ order for the change to take effect."
 
   ;; Big/small, black/white.
 
-  ("t" . ,(lean-input-to-string-list "▸▹►▻◂◃◄◅▴▵▾▿◢◿◣◺◤◸◥◹"))
-  ("Tr" . ,(lean-input-to-string-list "◀◁▶▷▲△▼▽◬◭◮"))
-  ("transport" . ("▹"))
+  ("t"     . ,(lean-input-to-string-list "▸▹►▻◂◃◄◅▴▵▾▿◢◿◣◺◤◸◥◹"))
+  ("Tr"    . ,(lean-input-to-string-list "◀◁▶▷▲△▼▽◬◭◮"))
 
   ("tb" . ,(lean-input-to-string-list "◂▸▴▾◄►◢◣◤◥"))
   ("tw" . ,(lean-input-to-string-list "◃▹▵▿◅▻◿◺◸◹"))
@@ -661,7 +664,7 @@ order for the change to take effect."
   ;; \omicron \Omicron
   ;; \pi \Pi
   ("Gr"  . ("ρ"))  ("GR"  . ("Ρ"))
-  ("Gs"  . ("σ"))  ("GS"  . ("Σ"))
+  ("Gs"  . ("σ"))  ("GS"  . ("Σ")) ("S"  . ("Σ"))
   ("Gt"  . ("τ"))  ("GT"  . ("Τ"))
   ("Gu"  . ("υ"))  ("GU"  . ("Υ"))
   ("Gf"  . ("φ"))  ("GF"  . ("Φ"))