Re: [isabelle] undefined & None

On 15.07.2013 07:47, Lars Noschinski wrote:
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, [...]

Stephan alerted me that "equivalent" is misleading here: They are "equivalent" in the sense that both can fill the same role, i.e., they represent an arbitrary value of type 'a. They are not "equivalent" in that we cannot prove any relation between "undefined :: 'a" and "SOME (x :: 'a). True.

  -- Lars

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