# Re: [isabelle] "Coercion inference failed"

On Wed, 30 Mar 2011, egglue at gmail.com wrote:

axiomatization
f :: "'a => 'b" and
g :: "nat => nat" where
ax : "f = g"

Why are 'a and 'b fixed under "axiomatization"?

`The specification is considered as one logical unit, where f and g are
``always the same local entity, with fixed types. The context is
``essentially this:
`
fix_type 'a and 'b -- "implicit"
fix g :: "'a => 'b" and g :: "nat => nat"
assume ax : "f = g"

`Later the types become arbitrary in the result, so the consts f and g in
``the target context can be used at different type.
`

`It is always the same game. This is how naive polymorphism works. There
``is no type quantification. (It would make the logic very complicated, or
``break down).
`

`It seems that I can
``produce very much the same declaration with:
`
axiomatization
f:: "'a => 'b" and
g :: "nat => nat"
axioms
ax : "f = g"
Why is f polymorphic in "axioms" but not in "axiomatization"?

'axioms' is an obsolete form, better do it like this:
axiomatization
f :: "'a => 'b" and
g :: "nat => nat"
axiomatization where
ax : "f = g"

`Separate specifications have separate scopes wrt. polymorphism. The
``consts axiomatized in the first one can be used at different types at the
``second one.
`
Makarius

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