Remove all files, redirect to GitHub.HEADmaster

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