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/SnocList.idr | 43 -------------------------------------------
 1 file changed, 43 deletions(-)
 delete mode 100644 src/Inky/Data/SnocList.idr

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

diff --git a/src/Inky/Data/SnocList.idr b/src/Inky/Data/SnocList.idr
deleted file mode 100644
index 494e8cc..0000000
--- a/src/Inky/Data/SnocList.idr
+++ /dev/null
@@ -1,43 +0,0 @@
-module Inky.Data.SnocList
-
-import public Data.SnocList
-import public Data.SnocList.Operations
-
-import Inky.Decidable.Maybe
-
-public export
-data LengthOf : SnocList a -> Type where
-  Z : LengthOf [<]
-  S : LengthOf sx -> LengthOf (sx :< x)
-
-%name LengthOf len
-
-public export
-lengthOfAppend : LengthOf sx -> LengthOf sy -> LengthOf (sx ++ sy)
-lengthOfAppend len1 Z = len1
-lengthOfAppend len1 (S len2) = S (lengthOfAppend len1 len2)
-
-public export
-lengthOf : (sx : SnocList a) -> LengthOf sx
-lengthOf [<] = Z
-lengthOf (sx :< x) = S (lengthOf sx)
-
-export
-lengthUnique : (len1, len2 : LengthOf sx) -> len1 = len2
-lengthUnique Z Z = Refl
-lengthUnique (S len1) (S len2) = cong S $ lengthUnique len1 len2
-
-export
-isSnoc : (sx : SnocList a) -> Proof (SnocList a, a) (\syy => sx = fst syy :< snd syy) (sx = [<])
-isSnoc [<] = Nothing `Because` Refl
-isSnoc (sx :< x) = Just (sx, x) `Because` Refl
-
-public export
-replicate : Nat -> a -> SnocList a
-replicate 0 x = [<]
-replicate (S n) x = replicate n x :< x
-
-public export
-lengthOfReplicate : (n : Nat) -> (0 x : a) -> LengthOf (replicate n x)
-lengthOfReplicate 0 x = Z
-lengthOfReplicate (S k) x = S (lengthOfReplicate k x)
-- 
cgit v1.2.3