Re: [isabelle] Type Coercions?

(Isn't "real (m+n)" equal to "real m + real n" anyway, so that it makes
no difference in the above example?)

If you don't have unification modulo "real (m+n) = real m + real n", I guess then it can make a difference :-)


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