What is the difference between willundefined and arbitrary?
Larry
On 2 Oct 2008, at 18:44, Tobias Nipkow wrote:
undefined and default are used in a specific way. If you do not
want
that functionality (and accidental equalities), arbitrary is a good
alternative.
Tobias
Florian Haftmann
Apologies for that garbled message. I meant,
What is the difference between undefined and arbitrary?
Larry
On 2 Oct 2008, at 18:44, Tobias Nipkow wrote:
undefined and default are used in a specific way. If you do not
want
that functionality (and accidental equalities), arbitrary
On Fri, 2008-10-03 at 14:14 +0200, Florian Haftmann wrote:
I also think that two would be better than three; technically
undefined is the same as arbitrary
Then what is the point of
undefined_fun: undefined x = undefined
in HOL.thy?
Best,
Tjark
Then what is the point of
undefined_fun: undefined x = undefined
in HOL.thy?
This is essentially pointless and is so soon to be dropped that I didn't
take the effort to even point out to it in my emails, taking the risk
that somebody would have a look a the source ;-)
Florian
Some years ago two further constants were introduces into HOL.thy:
undefined and default. The idea then was to divide the role of
classical arbitrary on two shoulders: undefined should be
unspecified an could be used to fake partiality, whereas default would
be overloaded and could be
undefined and default are used in a specific way. If you do not want
that functionality (and accidental equalities), arbitrary is a good
alternative.
Tobias
Florian Haftmann schrieb:
Some years ago two further constants were introduces into HOL.thy:
undefined and default. The idea then was to