Unicode Math Lean Symbols
lean-symbolsBy Johannes C. MayerInsert symbols like ∑ Π α → ↦ Γ etc, the same set of symbols as the VScode lean4 extension allows you to insert, using the same shortcuts. For example '\a\', '\a ', '\aTAB', all insert α, i.e. the greek alpha. TAB denotes a single press of the tab key.
math
symbols
Paste this command in a terminal to install the package
espanso install lean-symbolsSource
package.yml
custom_non_overriding_map.yml
matches:
- triggers:
- \{}\
- "\\{}\t"
replace: '{$CURSOR}'
- triggers:
- '\{} '
replace: '{$CURSOR} '
- triggers:
- \{}_\
- "\\{}_\t"
replace: '{$CURSOR}_'
- triggers:
- '\{}_ '
replace: '{$CURSOR}_ '
- triggers:
- \{{}}\
- "\\{{}}\t"
replace: ⦃$CURSOR⦄
- triggers:
- '\{{}} '
replace: '⦃$CURSOR⦄ '
- triggers:
- \[]\
- "\\[]\t"
replace: '[$CURSOR]'
- triggers:
- '\[] '
replace: '[$CURSOR] '
- triggers:
- \[]_\
- "\\[]_\t"
replace: '[$CURSOR]_'
- triggers:
- '\[]_ '
replace: '[$CURSOR]_ '
- triggers:
- \[[]]\
- "\\[[]]\t"
replace: ⟦$CURSOR⟧
- triggers:
- '\[[]] '
replace: '⟦$CURSOR⟧ '
- triggers:
- \<>\
- "\\<>\t"
replace: ⟨$CURSOR⟩
- triggers:
- '\<> '
replace: '⟨$CURSOR⟩ '
- triggers:
- \()\
- "\\()\t"
replace: ($CURSOR)
- triggers:
- '\() '
replace: '($CURSOR) '
- triggers:
- \()_\
- "\\()_\t"
replace: ($CURSOR)_
- triggers:
- '\()_ '
replace: '($CURSOR)_ '
- triggers:
- \([])'\
- "\\([])'\t"
replace: ⟮$CURSOR⟯
- triggers:
- '\([])'' '
replace: '⟮$CURSOR⟯ '
- triggers:
- \f<>\
- "\\f<>\t"
replace: ‹$CURSOR›
- triggers:
- '\f<> '
replace: '‹$CURSOR› '
- triggers:
- \f<<>>\
- "\\f<<>>\t"
replace: «$CURSOR»
- triggers:
- '\f<<>> '
replace: '«$CURSOR» '
- triggers:
- \[--]\
- "\\[--]\t"
replace: ⁅$CURSOR⁆
- triggers:
- '\[--] '
replace: '⁅$CURSOR⁆ '
- triggers:
- \nnnorm\
- "\\nnnorm\t"
replace: ‖$CURSOR‖₊
- triggers:
- '\nnnorm '
replace: '‖$CURSOR‖₊ '
- triggers:Show more