Re: [isabelle] undefined & None

Hi Stephan,

Thanks a lot for your clear answer. Just to be sure: I suppose you mean SOME ?

==> "(undefined::'a) = SOME (x::'a). True") ?


Le 14 juil. 2013 à 12:18, John Wickerson a écrit :

>> Note that in theory Hilbert_Choice one could actually define
>> definition undefined where "(undefined::'a) = Some (x::'a). True"

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