feat(abbreviations.json): Add abbreviation for Spec -> `𝖲𝗉𝖾𝖼`

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant

Apache License 2.0

158 stars 48 forks source link

feat(abbreviations.json): Add abbreviation for Spec -> `𝖲𝗉𝖾𝖼` #483

Closed erdOne closed 3 months ago

erdOne commented 3 months ago

Corresponding to the new notation introduced in https://github.com/leanprover-community/mathlib4/pull/14025

mhuisi commented 3 months ago

Please discuss this notation on Zulip first. I'm not sure if we really want to add abbreviations that are almost indistinguishable from regular editor text, but I'm happy to merge this if the Mathlib community agrees that this is the notation they want.

erdOne commented 3 months ago

Closing this as the notation is removed.