Ctrl+P
redtt-diagnostics
This extension adds a diagnostic functionality for redtt theorem prover.
redtt
You can also input Unicode symbols using LaTeX-like command and shape abbreviations.
Small cheatsheet for frequently used symbols:
\II
𝕀
\->
→
\Gl
λ
\#
★
\x
×
\6
∂
\\|-
⊢
\GO
Ω