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") ?

H.

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.