pub fn elaborate_term(
  term: elab_types.SurfaceTerm,
  ctx: elab_ctx.ElabCtx,
) -> Result(
  #(elab_ctx.ElabCtx, ast.Term),
  elab_types.ElaborateError,
)