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