[isabelle] undefined & None

Hi all,

I try to discover where the undefined value is ... defined. I could not find any undefined_def lemma or axiom.

In particular, is it polymorphic ? What are its properties ? What are the mathematical foundations and consequences of how it has been defined ?

I also wonder why the "None" option types constructor does not point to undefined in some way or another. Furthermore, I do not understand whether None is typed of not. 

This all sounds rather simple questions but I am a little ill at ease with using a keyword without its precise semantics in mind !

Thanks in advance

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