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

Version Path
tdiary-4.2.1 vendor/bundle/ruby/2.2.0/gems/pygments.rb-0.6.3/vendor/pygments-main/tests/examplefiles/example.lagda
pygments.rb-0.6.3 vendor/pygments-main/tests/examplefiles/example.lagda
pygments.rb-0.6.2 vendor/pygments-main/tests/examplefiles/example.lagda
pygments.rb-0.6.1 vendor/pygments-main/tests/examplefiles/example.lagda
pygments.rb-0.6.0 vendor/pygments-main/tests/examplefiles/example.lagda
mortar-pygments.rb-0.5.7 vendor/pygments-main/tests/examplefiles/example.lagda
mortar-pygments.rb-0.5.6 vendor/pygments-main/tests/examplefiles/example.lagda
mortar-pygments.rb-0.5.5 vendor/pygments-main/tests/examplefiles/example.lagda
pygments.rb-jruby-0.5.4.2 vendor/pygments-main/tests/examplefiles/example.lagda
pygments.rb-jruby-0.5.4.1 vendor/pygments-main/tests/examplefiles/example.lagda
pygments.rb-jruby-0.5.4 vendor/pygments-main/tests/examplefiles/example.lagda
gitlab-pygments.rb-0.5.4 vendor/pygments-main/tests/examplefiles/example.lagda
pygments.rb-0.5.4 vendor/pygments-main/tests/examplefiles/example.lagda