lean4-style-math-input README

This VS Code extension provides math unicode input snippets support for ∀ languages. Snippets are from the VS Code Lean 4 extension. 此 VS Code 扩展为任何语言提供了数学 Unicode 输入代码片段支持。代码片段来自 VS Code Lean 4 扩展。

Supported Features

Insert Symbols

Lean code uses a lot of Unicode symbols to improve readability. - But do you want to enjoy Unicode symbols in other languages? This extension brings the Unicode Input of the Lean plugin to any file. Lean 代码使用大量 Unicode 符号来提高可读性。——但是你想在别的语言里也享受 Unicode 符号？这个扩展把 Lean 插件的 Unicode Input 搬到了任何文件中。

By default, you can enter these Unicode symbols by typing a backslash followed by the abbreviation identifier for the symbol. For example, \forall will return ∀. 默认可以通过输入反斜杠加上指向该符号的缩写标识符来输入这些 Unicode 符号。例如，\forall 将返回 ∀。