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 (wkn1 _)
index (env :< t) (FS i) = wkn (index env i) (wkn1 _)

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' (wkn1 _)
indexCong (prf :< prf') (FS i) = wknCong (indexCong prf i) (wkn1 _)