Re: [isabelle] undefined & None



Oops, of course! -s

On Jul 14, 2013, at 12:42 PM, Henri DEBRAT <Henri.Debrat at loria.fr> wrote:

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