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, 14 insertions, 1 deletions

diff --git a/src/Inky/Context.idr b/src/Inky/Context.idr
index 2e9af8f..586aae2 100644
--- a/src/Inky/Context.idr
+++ b/src/Inky/Context.idr
@@ -70,6 +70,11 @@ public export
 ctx ++ [<] = ctx
 ctx ++ ctx' :< x = (ctx ++ ctx') :< x
 
+export
+appendLinLeftNeutral : (ctx : Context a) -> [<] ++ ctx = ctx
+appendLinLeftNeutral [<] = Refl
+appendLinLeftNeutral (ctx :< x) = cong (:< x) $ appendLinLeftNeutral ctx
+
 public export
 lengthAppend : Length ctx1 -> Length ctx2 -> Length (ctx1 ++ ctx2)
 lengthAppend len1 Z = len1
@@ -111,6 +116,14 @@ public export
 ThereVar : Var ctx v -> Var (ctx :< x) v
 ThereVar i = toVar (There i.pos)
 
+export
+Show (VarPos ctx x v) where
+  show i = show (toNat i)
+
+export
+Show (Var ctx v) where
+  show i = show i.pos
+
 -- Basic Properties
 
 export
@@ -237,7 +250,7 @@ namespace Quantifier
     Lin : All p [<]
     (:<) :
       All p ctx -> (px : Assoc0 (p x.value)) ->
-      {auto 0 prf : px.name = x.name}->
+      {auto 0 prf : px.name = x.name} ->
       All p (ctx :< x)
 
   %name Quantifier.All env