HomeIsabelle/Phabricator

Check inside the simplifier that the body of a potential inline function is…

Authored by dcjm on Thu, Jul 30, 1:40 PM.

Description

Check inside the simplifier that the body of a potential inline function is small. A function may be
marked as small enough to inline but if other functions have been inlined inside the body may now
be larger. In some cases that can lead to exponential blow-up. See issues #137 and #138.

Details

Committed
dcjmThu, Jul 30, 1:40 PM
Parents
rPOLYML6442ac3a51c6: Remove unused parameters.
Branches
Unknown
Tags
Unknown