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 :-)

Steven





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