[isabelle] Non terminating function proven terminating
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
fun f :: "unit \<Rightarrow> unit" where
"f x = (\<lambda> _ . ()) (f ())"
lemma fail : "f () \<equiv> ()"
This archive was generated by a fusion of
Pipermail (Mailman edition) and