Re: [isabelle] undefined & None
On 15.07.2013 07:47, Lars Noschinski wrote:
On 14.07.2013 11:22, Stephan Merz wrote:
Note that in theory Hilbert_Choice one could actually define
definition undefined where "(undefined::'a) = Some (x::'a). True"
That would be an equivalent definition, [...]
Stephan alerted me that "equivalent" is misleading here: They are
"equivalent" in the sense that both can fill the same role, i.e., they
represent an arbitrary value of type 'a. They are not "equivalent" in
that we cannot prove any relation between "undefined :: 'a" and "SOME (x
:: 'a). True.
This archive was generated by a fusion of
Pipermail (Mailman edition) and