# [isabelle] Overloading causes strange clash of specifications

Dear all,

`I am trying to overload a constant using the overloading target. 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"
overloading P' â "P :: (nat â 'a) â bool" begin
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.*