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



That is an excellent idea!
Larry

> On 27 Feb 2015, at 14:07, Johannes HÃlzl <hoelzl at in.tum.de> 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.