[isabelle] Polymorphism and type class



Hi,

If I have the following:

typedecl A
typedecl B

axiomatization
f :: "'a => nat"

axioms
ax1 : "f (x::A) = 0"
ax2 : "f (x::B) = 1"

Is the mechanism for "inspecting" the type of the argument of f
essentially defining a type class, or is it something else? If it's
indeed something else, then why isn't a type class used instead?

Any input will be appreciated. Thanks.

John





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