Restart.

- use De Bruijn, as Namely, Painless had more pain than promised;
- remove higher-kinded types;
- provide ill-typing predicates;
- prove substitution respects ill-typing;

1 files changed, 0 insertions, 30 deletions

diff --git a/src/Inky/Env.idr b/src/Inky/Env.idr
deleted file mode 100644
index 174b681..0000000
--- a/src/Inky/Env.idr
+++ /dev/null
@@ -1,30 +0,0 @@
-module Inky.Env
-
-import Control.Relation
-import Inky.Binding
-
-infix 2 :~
-
-public export
-record Assoc (0 a : Type) where
-  constructor (:~)
-  binder : Binder
-  value : a
-
-public export
-data PartialEnv : Type -> World -> World -> Type where
-  Lin : PartialEnv a w w
-  (:<) : PartialEnv a w v -> (x : Assoc a) -> PartialEnv a (w :< x.binder) v
-
-public export
-Env : Type -> World -> Type
-Env a w = PartialEnv a w [<]
-
-public export
-partialLookup : PartialEnv a w v -> Name w -> Either (Name v) a
-partialLookup [<] = Left
-partialLookup (env :< (x :~ v)) = stripWith (Right v) (partialLookup env)
-
-public export
-lookup : Env a w -> Name w -> a
-lookup = either absurd id .: partialLookup