Hi Lucas,
Nice failure :-)
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.
*)
This is the termination prover looping. It keeps
On 06/12/2010 15:15, Makarius wrote:
On Sun, 5 Dec 2010, Lucas Dixon wrote:
While playing around with a robotic horror that throw strange monsters
at the function package, I came across this rather strange error...
My guess is that some accidental infinite loop makes something bad
happen at a
On Mon, 6 Dec 2010, Lucas Dixon wrote:
... at the moment I need Isabelle2009-2, too many dependencies to
quickly unravel... is there an easy way to disable
multi-threading/futures so that I can see what the real ML error is? a
quick pointer to what to hack in the ML-Systems dir? :)
At the
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
