Function whnf_term 

pub fn whnf_term(node: &Node, env: &mut Env, options: ConvertOptions) -> Node

Weak-head normal form (D4): reduce the spine of node — i.e. unfold the head as long as there are arguments to apply to it — without descending into binders or argument positions. Mirrors whnfTerm in the JS runtime and nf/is_convertible already use normalize_term for the full version. Substitution may expose a redex inside the residual body, but that is no longer on the original spine, so this routine returns it unevaluated; full normalization is the place that descends into those positions.