Expand description
Evaluation: terms to values, application, and the values of constants.
Evaluation is call-by-value and performs β only. An application of a variable, a constant or a stuck projection becomes a neutral; δ and ι are left to weak-head reduction. So evaluating a term costs time proportional to the part of it outside every binder — a lambda is a closure whose body is not looked at until the closure is applied.
An expression is evaluated in its environment pruned to the entries it can see (the others are replaced by a placeholder), so that two environments agreeing on those entries give the same key for the evaluation cache and the same closure, and a closure is open exactly when something it can see is.
A universe-polymorphic constant’s type, body and recursor rules are evaluated from its own terms under the substitution of one use’s levels for its parameters, which the environment carries: sorts and constants take their levels through it as evaluation reaches them, and nothing is instantiated in advance. A term that mentions no universe parameter is read under the identity, so its value is shared by every instantiation.