Email Gateway (Aug 22 2022 at 09:22): Email Gateway (Aug 22 2022 at 09:22):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I found an issue in some internal tactic in the function package. Here's
a minimal example:
function iter_transform :: "'a ⇒ 'a" where
"iter_transform rs = (if True then iter_transform rs else rs)"
by pat_completeness auto
The problem appears to be the 'True'; if I replace it with 'undefined',
the error goes away.
(I know that the function as stated does not terminate, but that's not
the issue here.)
Cheers
Lars
Last updated: Apr 20 2024 at 01:05 UTC