3.2. Typing Contexts🔗

A context is a list of variable declarations. Lookup returns the type assigned to the first matching variable name.

\Gamma ::= \cdot \mid \Gamma, x : A

Contexts are lists, so the most recent declaration is checked first. This matches the usual convention that an inner binder shadows an outer one.

abbrev Context := List (String × Ty)

def lookup (x : String) : Context -> Option Ty
  | [] => none
  | (y, A) :: Γ => if x = y then some A else lookup x Γ