Re: [isabelle] Product or function?

A further difference I have not seen mentioned so far is that in the set of pairs case, also the domain of the graph is encoded, whereas in the function representation the domain is essentially all of the reals.


On 26.04.2012, at 06:31, John Munroe <munddr at> wrote:

> Hi
> If I want to model a line graph, should I give it the type of a product
> (real * real) or a function (real => real)? With a product type, would the
> graph be perceived as a set of pairs?
> Thanks for the help in advance.
> John

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