Re: [isabelle] "Coercion inference failed"



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.


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

lemma "f = g"

Here f is polymorphic and can be instantiated to "nat => nat".


	Makarius






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