From cf19cb0790a4efc1e6651b6aed31e67aab887e4d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Jul 2019 08:13:50 -0700 Subject: [PATCH] chore(lean4-mode/lean4-input): fix `\cdot` --- lean4-mode/lean4-input.el | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/lean4-mode/lean4-input.el b/lean4-mode/lean4-input.el index cfbc04da0c..23fe2fe7eb 100644 --- a/lean4-mode/lean4-input.el +++ b/lean4-mode/lean4-input.el @@ -333,8 +333,7 @@ order for the change to take effect." ("trans" . ,(lean4-input-to-string-list "▹⬝")) ("transport" . ("▹")) ("con" . ("⬝")) - ("cdot" . ("⬝")) - ("dot" . ("⬝")) + ("dot" . ("·")) ("sy" . ("⁻¹")) ("inv" . ("⁻¹")) ("-1" . ("⁻¹" "₋₁"))