From 3caa95a139538bb07c74847ca3aba2603a03c502 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 15 Nov 2024 15:44:30 +0000
Subject: Add compilation to scheme.

Extract parser as an independent project.
---
 src/Inky/Data/List.idr | 13 -------------
 1 file changed, 13 deletions(-)
 delete mode 100644 src/Inky/Data/List.idr

(limited to 'src/Inky/Data/List.idr')

diff --git a/src/Inky/Data/List.idr b/src/Inky/Data/List.idr
deleted file mode 100644
index 24cb9c0..0000000
--- a/src/Inky/Data/List.idr
+++ /dev/null
@@ -1,13 +0,0 @@
-module Inky.Data.List
-
-public export
-data LengthOf : List a -> Type where
-  Z : LengthOf []
-  S : LengthOf xs -> LengthOf (x :: xs)
-
-%name LengthOf len
-
-public export
-lengthOf : (xs : List a) -> LengthOf xs
-lengthOf [] = Z
-lengthOf (x :: xs) = S (lengthOf xs)
-- 
cgit v1.2.3