Module whnf 

Weak-head reduction of values: ι (recursors, with K and struct-η), quotients, projections, validated Nat literal operations, and δ through constant heads.

β is already done by evaluation, so a value’s weak head can only be blocked by a recursor or quotient eliminator, a stuck projection, a literal operation, or a definition. Every step is remembered on the value that took it: the unfolding of a definition application, the whnf_core and whnf of any value.