[isabelle] undefined & None
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