------------------------------------------------------------------------
-- Environments
------------------------------------------------------------------------

-- This module could be replaced with Data.Star.Environment from the
-- standard libraries, but I don't want to depend too much on external
-- libraries in this development.

open import SimplyTyped.TypeSystem

module SimplyTyped.Environment (Contents : Ty  Set) where

infixl 20 _▷_

data Env : Ctxt  Set where
     : Env ε
  _▷_ :  {Γ τ}  Env Γ  Contents τ  Env (Γ  τ)

lookup :  {Γ τ}  Γ  τ  Env Γ  Contents τ
lookup vz     (ρ  v) = v
lookup (vs x) (ρ  v) = lookup x ρ