|
|
|---|
|
|
|
|---|
Theorem about find-fun and
If find-fun is successful on a function environment without function definitions in the bodies, the result has no function definitions in the bodies.
Theorem:
(defthm funinfo+funenv-nofunp-of-find-fun (implies (and (funenv-nofunp funenv) (not (reserrp (find-fun fun funenv)))) (funinfo+funenv-nofunp (find-fun fun funenv))))