Expand description
Type inference and checking over values.
A term is walked with an environment (the values of its bound variables) and a context (their
types), and its type is produced as a value. An application’s type is its function type’s
closure instantiated with the argument’s value; crossing a binder binds a fresh variable; a
lambda’s type is a closure whose codomain is inferred only if something asks for it. With
check, every rule of the substitution checker is enforced — universe parameters, safety,
argument types, let values, the restrictions on projecting out of a proposition.