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.

1 files changed, 13 insertions, 0 deletions

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