[isabelle] function package: tactic failed
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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and