Function resolve_names_in 

pub fn resolve_names_in<'t>(
    ns: &Namespaces,
    env: &Env<'_>,
    locals: &mut Vec<String>,
    term: &'t Term,
) -> Result<Cow<'t, Term>, ParseError>

Resolve every global name written in term against the scope, BEFORE any elaboration sees it — Lean’s staging, and the whole content of “name resolution completes before translation begins”.

env is the environment (Env); locals is the stack of names that are BOUND here and so are not global references at all (an inductive’s type parameters arrive as Globals and become Vars only later, so they have to be shielded by hand).

Returns Cow::Borrowed when nothing in the term needed resolving, so an empty scope costs one read-only walk and not a rebuild.