Re: [isabelle] change proposal: eliminating overloading for factorials



Yes, nat + automatic coercion is better!

As a test, I replaced "real (fact" by "(fact" in
Transcendental and it works with one exception
(which has the wrong type: "2 * 2 ^ n â real (fact (n + 2))").
Dmitriy did a very good job :-) 

 - Johannes


Am Montag, den 02.03.2015, 12:16 +0000 schrieb Larry Paulson:
> I was wondering about this myself. Maybe type nat and automatic coercions are better?
> Larry
> 
> > On 2 Mar 2015, at 12:08, Johannes HÃlzl <hoelzl at in.tum.de> wrote:
> > 
> > I made the suggestion for fact as it is used a lot for transcendental
> > functions.
> 
> 






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