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