Agda is a dependently typed programming language / interactive theorem prover.
I am used to writing things on paper and hand-wave a lot of assumptions in my proofs. I want to learn Agda so that I can formalize my proofs. This in-progress article captures my journey learning Agda.
The VSCode agda integration was quirky - the language server als would not work at all and syntax highlighting only works on pressing C-c C-l and when the program is correct. I am not used to emacs or vim so I am going to stick to my existing workflow using Kate.
Since Kate does not natively support inserting unicode characters using LaTeX shorthands, I created an external tool in Kate that pipes the selected text to pandoc and gets the plaintext unicode output. This works as expected and is fairly snappy.
For example, $\lambda \mathbb N _2$ renders to λℕ₂ on pressing Ctrl+Shift+\ and this is how the browser renders the same sequence:
entr watches my agda files and runs agda when my changes are saved.
echo NowYouTry/GettingStarted.agda | entr -c agda NowYouTry/GettingStarted.agda