Matt Kaufmann wrote:
>
> It might be *very* useful to have a user-settable special variable
> that controls inlining. I'm imagining that by default, ACL2 would
> inline all built-in and user-defined function calls that GCL allows,
> but that when one wants to trace, then it would be nice to be able to
> rebuild with inlining turned down or off.
Isn't this what (declaim (inline foo)) is supposed to do? Granted, it's
tedious to specify this for every function foo that you want inlined,
but that seems to me the right thing to do too. I can't imagine wanting
to inline every single function! :-)
Ray