From 3f67fd69e48d27c6aa77f8b2c31159bbfb85e99a Mon Sep 17 00:00:00 2001
From: arienmalec <arien.malec@gmail.com>
Date: Tue, 21 May 2024 01:24:21 -0700
Subject: [PATCH] feat: add span abbreviation (#447)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds an abbreviation "span" for the Uncode "∙" used in
"Mathlib/LinearAlgebra/Span.lean"

See
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Show.20the.20basis.20vectors.20of.20R.5En.20sum.20to.20R.5En/near/439392547
---
 vscode-lean4/src/abbreviation/abbreviations.json | 1 +
 1 file changed, 1 insertion(+)

diff --git a/vscode-lean4/src/abbreviation/abbreviations.json b/vscode-lean4/src/abbreviation/abbreviations.json
index 3b9a5dc10..326b54d86 100644
--- a/vscode-lean4/src/abbreviation/abbreviations.json
+++ b/vscode-lean4/src/abbreviation/abbreviations.json
@@ -777,6 +777,7 @@
     "straightphi": "φ",
     "st": "⋆",
     "spesmilo": "₷",
+    "span": "∙",
     "spadesuit": "♠",
     "sphericalangle": "∢",
     "section": "§",