Re: [isabelle] Type for pairs
I've found a solution: use Cartesian product instead.
On Fri, Jun 4, 2010 at 12:23 PM, Eg Gloor <egglue at gmail.com> wrote:
> 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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and