From 3a23bd851fc1a5d6e161dabc8a13f06bc8544a1d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 9 Sep 2024 11:33:45 +0100
Subject: 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;
---
 src/Inky/Env.idr | 30 ------------------------------
 1 file changed, 30 deletions(-)
 delete mode 100644 src/Inky/Env.idr

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

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
-- 
cgit v1.2.3