Re: [isabelle] Infinitely recursive lambda expression or not?
It is simply that if f is the constant-True function, then f = (λa. False ∨ f False).
I think that you are imagining some sort of execution model for HOL. But HOL doesn’t have an operational semantics.
On 14 Dec 2013, at 13:26, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote:
> I wanted to check if had an issue with binding (indeed, I did had issues with implicit operations in some cases), so tried this:
> lemma "f = (λa. False ∨ f False) ⟹ (f False = False)"
> It still says it find a counter example, with “f False = True”. Precisely, what I don't understand, is why it suppose this may be True. “a” is not used, and the only constant used in f is False.
This archive was generated by a fusion of
Pipermail (Mailman edition) and