Function normalize_checked_elab 

pub fn normalize_checked_elab(
    ctx: &Context,
    term: &Term,
) -> Result<Term, (Term, Unreduced)>

The elaborator’s reduction face: @[irreducible] constants stay folded, body intact, with the opacity predicate built once from Context::is_irreducible rather than by each caller. normalize remains the kernel’s face and unfolds everything, exactly as Lean’s does. normalize_elab’s honest face: the elaborator’s transparency, and a reduction that did not finish reported as such rather than handed back as a normal form.