# Re: [isabelle] undefined & None

On 13.07.2013 23:17, Henri DEBRAT wrote:

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 ?

`You can see whether a term is polymorphic or not by simply printing it
``with "term" -- iff its type contains type variables, it is polymorphic
``(in the global context).
`
"undefined :: 'a" has exactly those properties any value of type 'a has.

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.

`Every value in Isabelle has exactly one concrete type, so None is
``"typed". A polymorphic constant like None can be used to refer to
``various values, depending on its type.
`
I.e., you can have e.g. "None :: nat option" and "None :: int option"
but if you write "(None :: nat option) = (None :: int option)" you get
a type error.
-- Lars

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