Fn-get-def
Look up a function's definition from the world.
Invocation:
(fn-get-def fnname state)
or equivalently,if world is (w state),
(fn-get-def-w fnname world)
produces (mv successp formals body), where if successp is true,
then (fnname . formals) is equal to body under evaluation.
fn-get-def can be assumed to work correctly in the context of
metafunctions and clause processors via meta-extract.
The def-meta-extract macro supports fn-get-def indirectly: we
rewrite the successp return value to a call of fn-check-def, and
def-meta-extract provides a theorem that rewrites an evaluation of
(fnname . args) to the evaluation of body under the pairing of
formals to args when it can relieve the hypothesis
(fn-check-def fnname state formals body).
