1\documentclass{article}
2% this is a LaTeX comment
3\usepackage{agda}
4
5\begin{document}
6
7Here's how you can define \emph{RGB} colors in Agda:
8
9\begin{code}
10module example where
11
12open import Data.Fin
13open import Data.Nat
14
15data Color : Set where
16    RGB : Fin 256 → Fin 256 → Fin 256 → Color
17\end{code}
18
19\end{document}