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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and