From ecaf9deb4b1d2ce85617438e621690b2df3ea367 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 12 Nov 2024 16:44:31 +0000
Subject: Add ability to desugar terms.

Remove `getChildren` construct---it's too niche for the core language.
---
 src/Inky/Data/List.idr | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create 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
new file mode 100644
index 0000000..24cb9c0
--- /dev/null
+++ b/src/Inky/Data/List.idr
@@ -0,0 +1,13 @@
+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