TypingRules

TOC

Contexts

A context tracks the variables in scope and their types. Contexts do not appear explicitly in Agda source code, but they do govern its meaning and can be queried during interactive development.

Specifically, a context is a list of type assignments x : a. Later (further to the right) bindings shadow earlier ones. These ideas can be captured formally in a definition of valid contexts. That a context Γ is valid is written Γ valid.

               Γ ⊢ S : Set[n]
 ----------  ------------------
  ℰ valid    Γ , x : S valid

ℰ denotes the empty context. TODO finish

Types

TODO

relationship to checking and inference algorithms?

forward references to things that extend these rules (e.g. Declarations).