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).

  -- Lars




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