Re: [isabelle] undefined & None
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, as would be
"SOME x. False" or "THE x. x = x".
However, mind that we cannot prove "undefined :: 'a" and "SOME x :: 'a.
True" to be equal (except for 'a = unit, of course).
This archive was generated by a fusion of
Pipermail (Mailman edition) and