[isabelle] Non terminating function proven terminating



Hi everyone,

I did not find Isabelle's bug tracker so I hope that this is the place where
I'm supposed to report this.

Pierre Boutillier's trick (which breaks Coq's SN) seems to work in Isabelle.
As in Agda, we do not lose SN but we do accept a function that is not
well-defined.

================================
theory test
imports Main

begin

fun f :: "unit \<Rightarrow> unit" where
  "f x = (\<lambda> _ .  ()) (f ())"

lemma fail : "f () \<equiv> ()"
by simp

end
================================

Cheers,

--
gallais





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.