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



> What about defining fact semi-polymorphic? Like
>   fact :: nat => 'a::semiring_1

The nice thing about this is that simple propositions involving numerals
are provable out of the box:

> context semiring_1
> begin
> 
> primrec factorial :: "nat â 'a"
> where
>   "factorial 0 = 1"
> | "factorial (Suc n) = of_nat (Suc n) * factorial n"
> 
> lemma "factorial 3 = 6"
>   by (simp add: eval_nat_numeral)
> 
> end

This is again one of the things where you ask yourself how it could have
been different in the past after you got used to it.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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