summaryrefslogtreecommitdiff
path: root/tests/examplefiles/example.lagda
diff options
context:
space:
mode:
Diffstat (limited to 'tests/examplefiles/example.lagda')
-rw-r--r--tests/examplefiles/example.lagda19
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