summaryrefslogtreecommitdiff
path: root/src/Inky/Env.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Inky/Env.idr')
-rw-r--r--src/Inky/Env.idr30
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