Function normalize_elab 

pub fn normalize_elab(ctx: &Context, term: &Term) -> Term

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 at the ELABORATOR’s transparency, reading the context’s own reducibility registry — the door that makes @[irreducible] reachable without every caller inventing its own opacity predicate.

Transparency::Excluding takes a PREDICATE so the reducer need not know how the attribute is stored; the cost of that freedom is that a caller has to build the closure, and two callers that build it differently would disagree about whether a constant unfolds — which is def_eq answering differently depending on who asked. This is the one closure, built from Context::is_irreducible, so there is nothing to get wrong.

FOLLOWING LEAN, INCLUDING WHERE IT IS SUBTLE: this is NOT what the kernel uses. Lean’s kernel unfolds every definition whatever its attribute — example : secret = 5 := rfl on an @[irreducible] def secret := 5 is refused by the elaborator and accepted by the kernel — so normalize stays Transparency::All and this is the elaborator’s face.