[isabelle] Isabelle functions: Always total, sometimes undefined



Hi,

based on repeated discussions and confusion when interacting with
functional programmers and type-theory based theorem prover users, I
wrote a blog post explaining how functions in Isabelle are different
than functions in Haskell/Coq/etc, and what the deal is about
undefined:

http://www.joachim-breitner.de/blog/732

Please let me know if I say something wrong that should not be said
like that on the Internet. Otherwise, feel free to share when you have
trouble explaining these things to someone.

Regards,
Joachim

-- 
Joachim Breitner
Post-Doctoral researcher
http://cis.upenn.edu/~joachim

Attachment: signature.asc
Description: This is a digitally signed message part



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