Define typing environments.

1 files changed, 40 insertions, 0 deletions

diff --git a/src/Core/Environment.idr b/src/Core/Environment.idr
new file mode 100644
index 0000000..f13cde3
--- /dev/null
+++ b/src/Core/Environment.idr
@@ -0,0 +1,40 @@
+module Core.Environment
+
+import Core.Term
+import Core.Term.Thinned
+import Core.Thinning
+
+infix 4 =~=
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Env : Nat -> Type where
+  Lin : Env 0
+  (:<) : Env n -> Thinned n -> Env (S n)
+
+namespace Eq
+  public export
+  data (=~=) : Env n -> Env n -> Type where
+    Refl : env =~= env
+    (:<) : env1 =~= env2 -> t =~= u -> env1 :< t =~= env2 :< u
+
+%name Env env
+%name Eq.(=~=) prf
+
+-- Indexing --------------------------------------------------------------------
+
+public export
+index : Env n -> Fin n -> Thinned n
+index (env :< t) FZ = wkn t (drop $ id _)
+index (env :< t) (FS i) = wkn (index env i) (drop $ id _)
+
+export
+indexCong :
+  {0 env1, env2 : Env n} ->
+  env1 =~= env2 ->
+  (i : Fin n) ->
+  index env1 i =~= index env2 i
+indexCong Refl i = Refl
+indexCong (prf :< prf') FZ = wknCong prf' (drop $ id _)
+indexCong (prf :< prf') (FS i) = wknCong (indexCong prf i) (drop $ id _)