Add ability to desugar terms.

Remove `getChildren` construct---it's too niche for the core language.

1 files changed, 13 insertions, 0 deletions

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)