Hi,
While playing around with a robotic horror that throw strange monsters
at the function package, I came across this rather strange error...
*** start of theory ***
theory fun_def_oddity
imports Main
begin
datatype Ta = C_2 "nat" "nat" | C_1 "Ta" "nat"
fun f where
"f (C_2 a b) c = c"
| "f (C_1 a b) c = f a (f a (f a (f (C_1 a b) b)))"
(* ... after a long time...
constants
f :: "Ta ⇒ nat ⇒ nat"
Exception.
At command "fun".
*)
end;
*** end of theory ***
Now I know this isn't a good looking function, but the error message
seems somewhat odd.
My guess is that some accidental infinite loop makes something bad
happen at a low level... but I've ever seen the "Exception." things
before, so I'm not too sure what to do next.
Moreover, (and importantly for me) when I'm calling this from ML, I'm
not sure how to catch the resulting error, it seems to be skipping past
my attempts to handle it. Any thoughts?
cheers,
lucas
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
