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 in.tum.de> wrote:
> I also second this proposal, the definition of fact_int is quite
> 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