# Re: [isabelle] how to state that a function is well-defined?

I’m afraid that this concept of "well-defined” does not exist in higher-order logic. You may find that some properties of foo only hold for non-empty lists, that’s all.
Larry Paulson
On 1 Nov 2013, at 18:41, John Wickerson <johnwickerson at cantab.net> wrote:
> This is a really basic question, and I'll probably kick myself once somebody tells me the answer.
>
> How can I state a lemma that simply says my function is "well-defined"? I mean: suppose I define
>
> definition "foo x == x ! 0"
>
> I want to say that foo is "well-defined" on all inputs other than the empty list. I'm imagining something like
>
> lemma "x ≠ [] ⟹ ∃!y. foo x = y"
>
> but that's true for any foo.
>
> Thanks!
>
> john
>
>

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