Test files for Agda and literate Agda mode

1 files changed, 19 insertions, 0 deletions

diff --git a/tests/examplefiles/example.lagda b/tests/examplefiles/example.lagda
new file mode 100644
index 00000000..b5476fa0
--- /dev/null
+++ b/tests/examplefiles/example.lagda
@@ -0,0 +1,19 @@
+\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