Re: [isabelle] "Coercion inference failed"



On Mar 30, 2011 6:24pm, Makarius <makarius at sketis.net> wrote:
On Wed, 30 Mar 2011, Eg Gloor wrote:




axiomatization

f :: "'a => 'b" and

g :: "nat => nat" where

ax : "f = g"




Here 'a and 'b are fixed in the scope where "f = g" needs to type check.


I see. Why are 'a and 'b fixed under "axiomatization"? 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"?

Thanks

Eg




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