Sha256: 8715f69200007f801141e3c3d22d1323356a44114a80ff6c532006193d3735f2
Contents?: true
Size: 320 Bytes
Versions: 13
Compression:
Stored size: 320 Bytes
Contents
\documentclass{article} % this is a LaTeX comment \usepackage{agda} \begin{document} Here's how you can define \emph{RGB} colors in Agda: \begin{code} module example where open import Data.Fin open import Data.Nat data Color : Set where RGB : Fin 256 → Fin 256 → Fin 256 → Color \end{code} \end{document}
Version data entries
13 entries across 13 versions & 5 rubygems