HomeIsabelle/Phabricator

When analysing the usage pattern of a recursive function we need to consider…

Description

When analysing the usage pattern of a recursive function we need to consider the way the result is used in
both non-recursive and recursive calls. This may require reanalysis of the body. To check whether reanalysis
is necessary we need a fully recursive comparison of the usage patterns. The previous code did not go deeply
enough. It turns out that 744d14 avoided the problem but did not properly solve it.

Details

Provenance
dcjmAuthored on Jul 6 2020, 9:30 AM
Parents
rPOLYML7edf731ebd7f: Fix use of "print" rather than "stream" for debugging.
Branches
Unknown
Tags
Unknown