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.