From 8b326bb4a879be72cb6382519350cbb5231f7a6e Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 9 Oct 2024 16:26:23 +0100
Subject: Do a lot.

- Add type aliases.
- Make `suc` a symbol.
- Fix incorrect specification for `IsFunction`.
- Write parser for terms.
- Use `collie` to improve command line experience.
---
 src/Inky/Type.idr | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'src/Inky/Type.idr')

diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index 9cfc1f7..26f3c0f 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -406,3 +406,16 @@ subAll env ((:<) as (x :- a) {fresh}) =
 
 subAllFresh env x [<] = id
 subAllFresh env x (as :< (y :- a)) = andSo . mapSnd (subAllFresh env x as) . soAnd
+
+-- Expansion -------------------------------------------------------------------
+
+export
+expandEnv : DEnv Ty ctx -> Env ctx [<] (Ty [<])
+expandEnv [<] = Base Id
+expandEnv {ctx = ctx :< (x :- v)} (env :< (y :- a)) =
+  let env' = expandEnv env in
+  expandEnv env :< (x :- sub env' a)
+
+export
+expand : DEnv Ty ctx -> Ty ctx v -> Ty [<] v
+expand = sub . expandEnv
-- 
cgit v1.2.3