Ground-term reduction and symbolic evaluation

What question should the reference manual answer?

The simplifier is apparently able to do things like "ground-term reduction" using simp +ground, and there is apparently something called "symbolic evaluation" which might have something to do with the seval simp set, but I cannot find an explanation of this anywhere. What do these do? When might I use them? How are the two concepts related?

Advanced bonus questions (which are the actual questions I have but I cannot even start trying to find answers because I don't even know how to answer the questions above): in what way do I need to be aware of ground-term reduction and symbolic evaluation when writing simprocs? What is an sevalproc?

Additional context
The chapter on simp contains the docstring for the +ground option to simp, but this is not helpful to me if I don't know what it is talking about.

There are reasons to believe that ground-term reduction is relevant when writing simprocs as we have code like this:

/-- Return `.done` for Nat values. We don't want to unfold in the symbolic evaluator. -/
builtin_dsimproc [seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do
  let_expr OfNat.ofNat _ _ _ ← e | return .continue
  return .done e

We also have this:

builtin_dsimproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do
  let_expr Neg.neg _ _ arg ← e | return .continue
  if arg.isAppOfArity ``OfNat.ofNat 3 then
    -- We return .done to ensure `Neg.neg` is not unfolded even when `ground := true`.
    return .done e
  else
    let some v ← fromExpr? arg | return .continue
    return .done <| toExpr (- v)

I feel that understanding why this code is needed is required for writing your own simprocs for numeric types.

Start with the reference manual's chapter on simp and its +ground option docstring, then investigate the seval simp set, simprocs, and sevalprocs shown in the issue. Done means documenting ground-term reduction and symbolic evaluation, their relationship and use cases, and how they affect numeric simprocs, including why the examples return .done.