Definition rules of the
It may seem surprising that we expand these functions,
since those correspond to C constructs;
we certainly do not expand functions like add-sint-sint.
The reason is that functions like sint-dec-const
are used to represent C constants in ACL2 functions,
but in the dynamic semantics,
exec-const (which we expand, obviously)
produces terms of the form