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}