diff options
Diffstat (limited to 'tests/examplefiles/example.lagda')
-rw-r--r-- | tests/examplefiles/example.lagda | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/tests/examplefiles/example.lagda b/tests/examplefiles/example.lagda deleted file mode 100644 index b5476fa0..00000000 --- a/tests/examplefiles/example.lagda +++ /dev/null @@ -1,19 +0,0 @@ -\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}
\ No newline at end of file |