Re: [isabelle] Type for pairs



I've found a solution: use Cartesian product instead.

Thanks
Eg

On Fri, Jun 4, 2010 at 12:23 PM, Eg Gloor <egglue at gmail.com> wrote:

> Hello,
>
> I'm trying to define a type for representing a graph and think a type for a
> pair of functions would be suitable. How do I do that? I've tried
>
> datatype graph = "('a, 'b)"
>
> But then
>
> consts
> grph1 :: graph
> a :: "nat => nat"
> b :: "nat => nat"
> ...
>
> "grph1 = (a x, b x)" as an axiom complains about clash of types "*" and
> "graph". I must be doing something wrong here.
>
> Thanks for the help.
> Eg
>




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