1 files changed, 0 insertions, 90 deletions
diff --git a/src/Inky/Data/SnocList/Var.idr b/src/Inky/Data/SnocList/Var.idr
deleted file mode 100644
index cc7c088..0000000
--- a/src/Inky/Data/SnocList/Var.idr
+++ /dev/null
@@ -1,90 +0,0 @@
-module Inky.Data.SnocList.Var
-
-import public Inky.Data.SnocList.Elem
-
-import Data.Singleton
-import Inky.Data.SnocList
-import Inky.Decidable
-
-export
-prefix 2 %%
-
-public export
-record Var (sx : SnocList a) where
-  constructor (%%)
-  0 name : a
-  {auto pos : Elem name sx}
-
-%name Var i, j, k
-
-public export
-toVar : Elem x sx -> Var sx
-toVar pos = (%%) x {pos}
-
-public export
-ThereVar : Var sx -> Var (sx :< x)
-ThereVar i = toVar (There i.pos)
-
-export
-Show (Var sx) where
-  show i = show (elemToNat i.pos)
-
--- Basic Properties ---------------------------------------------------------
-
-export
-toVarCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> toVar i = toVar j
-toVarCong Refl = Refl
-
-export
-posCong : {0 i, j : Var sx} -> i = j -> i.pos ~=~ j.pos
-posCong Refl = Refl
-
-export
-toVarInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : toVar i = toVar j) -> i = j
-toVarInjective prf = toNatInjective $ toNatCong $ posCong prf
-
-export
-posInjective : {i : Var sx} -> {j : Var sx} -> (0 _ : i.pos ~=~ j.pos) -> i = j
-posInjective {i = %% x} {j = %% y} prf = irrelevantEq $ toVarCong prf
-
--- Decidable Equality ----------------------------------------------------------
-
-public export
-DecEq' (Var {a} sx) where
-  does i j = (decEq i.pos j.pos).does
-  reason i j =
-    mapWhen (\prf => irrelevantEq $ posInjective prf) posCong $
-    (decEq i.pos j.pos).reason
-
--- Weakening -------------------------------------------------------------------
-
-public export
-wknL : (len : LengthOf sy) => Var sx -> Var (sx ++ sy)
-wknL i = toVar $ wknL i.pos len
-
-public export
-wknR : Var sx -> Var (sy ++ sx)
-wknR i = toVar $ wknR i.pos
-
-public export
-split : {auto len : LengthOf sy} -> Var (sx ++ sy) -> Either (Var sx) (Var sy)
-split i = bimap toVar toVar $ split len i.pos
-
-public export
-lift1 :
-  (Var sx -> Var sy) ->
-  Var (sx :< x) -> Var (sy :< y)
-lift1 f ((%%) x {pos = Here}) = %% y
-lift1 f ((%%) name {pos = There i}) = ThereVar (f $ %% name)
-
--- Names -----------------------------------------------------------------------
-
-export
-nameOf : {sx : SnocList a} -> (i : Var sx) -> Singleton i.name
-nameOf i = nameOf i.pos
-
--- Search ----------------------------------------------------------------------
-
-export
-lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Var sx)
-lookup x sx = toVar <$> lookup x sx