# Tutorials

## Every-day Unicode

Following this tutorial you can have any symbol at your fingertip when typing on a Linux or *BSD system.

## Unicode for mathematics symbols in LaTeX

Write readable LaTeX files, with $A = πr²$ instead of $A = \pi r^2$ in the source.

## Writing Agda-code in another edtior

Agda, is a dependently typed language for programming and proof-verification. Here is how I write it, using the Acme editor.