The evaluation semantics of ACL2 is formalized here in terms of a succession of the evaluation states formalized by the fixtype eval-state. This is a small-step operational semantics, from which we could also define a big-step operational semantics (by composing the small steps).
A small-step semantics is more flexible than a big-step semantics, because it lets us talk about intermediate evaluation states, and not just the final states. This is particularly important to describe non-terminating executions. Also, we can easily derive a big-step semantics from a small-step one, but not vice versa.
There are different options for the granularity of the (small) steps. The granularity that we formalize here should be adequate, but it can be changed if needed or useful.