Literate Programming in Aya
This is based on (outdated) Introduction to literate Aya and code snippets from haskeller-tutorial.aya.
Defining a type
open inductive Nat | zero | suc Nat

Defining an operation
example def infixl <+> Nat Nat : Nat
| 0, n ⇒ n
| suc m, n ⇒ suc (m <+> n)

overlap def infixl <+> Nat Nat : Nat
| 0, n ⇒ n
| n, 0 ⇒ n
| suc m, n ⇒ suc (m <+> n)

Meta-variables
example def infixl [+] (a n : Nat) : Nat elim a
| 0 ⇒ n
| suc m ⇒ suc {??}

Compilation errors
def foo ⇒

Math formulas
\[

\begin{align*}
\Gamma,\Delta,\Theta ::=  & \quad \varnothing      \\[-0.3em]
                     \mid & \quad \Gamma , x : A   \\[-0.3em]
\Sigma         ::=  & \quad \varnothing            \\[-0.3em]
               \mid & \quad \Sigma,\mathrm{decl}   \\[-0.3em]
\end{align*}

\]