Re: [isabelle] Isabelle functions: Always total, sometimes undefined



On 12/10/17 20:18, Joachim Breitner wrote:
> 
> http://www.joachim-breitner.de/blog/732

I generally like it. Yes, HOL is first and foremost classical
mathematics; the functional specifications give an appearance of
functional programming, without restricting it to a computational
world-view. The "programming" in HOL is good enough for most applications.

BTW, if you take the literal meaning of the word "undefined", it means
"not defined". So it fits well into your story. People who think of
"undefined" as "halt and catch fire" instruction are wrong :-)

Minor note: some ASCII => have sneaked in, but you appear to use Unicode
rendering of Isabelle symbols uniformly.


	Makarius

Attachment: signature.asc
Description: OpenPGP digital signature



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