pub fn surface_elaborate(ctx: &Context, term: &Term) -> KernelResult<Term>Expand description
Elaborate a whole surface term: walk it, and at every application of a global with
declared implicit parameters (Context::implicit_args), insert and infer those
arguments — so id 0 becomes id Int 0. Terms with no implicits are returned
unchanged. The result is fully explicit and metavariable-free; the kernel certifies
it as usual. This is the seam that wires the elaborator into the REPL.