------------------------------------------------------------------------ -- 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 ρ