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

That is an excellent idea!

> On 27 Feb 2015, at 14:07, Johannes HÃlzl <hoelzl at> wrote:
> I also second this proposal, the definition of fact_int is quite
> strange.
> What about defining fact semi-polymorphic? Like
>  fact :: nat => 'a::semiring_1
> then we do not need to depend on coercions, only on typeclasses. And in
> semiring_1 the defining fact-equations should hold. 

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