Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] fun package raises exceptions on the following...

Email Gateway (Jan 29 2026 at 12:20):

From: i n <cl-isabelle-users@lists.cam.ac.uk>

Hi all,
I've noticed that the function package raises an exception in the following functionfunction test :: "nat ⇒ nat" where
"test n = (if n = 0 then 0 else
          let x = (λn. test n) in
          test (x (n - 1)))"After posting this on the zulip see https://isabelle.zulipchat.com/#narrow/channel/202961-General/topic/Isabelle's.20fun.20package.20raises.20an.20exception/
Fabian Huch managed to reduce it to the followingfun f :: "nat ⇒ nat" where
  "f 0 = 0" |
  "f _ = (let x = f in f 0)"Thanks,
Irvin

Last updated: Jan 31 2026 at 12:53 UTC