```Hi Ondrej,

```
Thanks for the hint. In the single-parameter case, I had added the type constraints, which made it go through, but I forgot to do the same for the two-parameter case.
```
```
Still, I wonder why they are necessary in the first place. In the end, I have already fixed the type of R' in the overloading part.
```
Best,
Andreas

On 01/06/15 14:40, OndÅej KunÄar wrote:
```
```Hi Andreas,
the problem is that R in R_nat_def is defined with type "('c => 'd) => ('c => 'e) => bool".

The following works around the problem:

overloading R' â "R :: (nat â 'a) â (nat â 'b) â bool"  begin
definition R_nat_def: "(R':: (nat â 'a) â (nat â 'b) â bool) f g = (âx. R (f x) (g x))"
end

Ondrej

On 06/01/2015 01:58 PM, Andreas Lochbihler wrote:
```
```Dear all,

However, I get an error that my specifications clash, even though I
cannot see why. Here is the minimised example:

consts R :: "'a â 'b â bool"

overloading R' â "R :: (nat â 'a) â (nat â 'b) â bool"  begin
definition R_nat_def: "R' f g = (âx. R (f x) (g x))"
end

overloading R' â "R :: ('a list â 'b) â ('c list â 'd) â bool" begin
definition R_list_def: "R' f g = (âxs ys. R (f xs) (g ys))"
end

The second definition raises the error, but the two definitions should
be fine as the types of the overloaded constant cannot be unified and
the recursive calls to R occur only at smaller types. Interestingly, if
I throw out one parameter, everything works fine:

consts P :: "'a â bool"

definition P_nat_def: "P' (f :: nat â 'a) = (âx. P (f x))"
end

overloading P' â "P :: ('b list â 'a) â bool" begin
definition P_list_def: "P' (f :: 'b list â 'a) = (âx. P (f x))"
end

So what is going on here? Why does the two parameter-case fail? And how
can I avoid the failure?

Thanks in advance for any hints,
Andreas

```
```

```
```

```

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