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