Re: [isabelle] change proposal: eliminating overloading for factorials
Presumably for the Fibonacci numbers too? Currently
fun fib :: "nat \<Rightarrow> nat"
fib0: "fib 0 = 0"
| fib1: "fib (Suc 0) = 1"
| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
> On 28 Feb 2015, at 08:18, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>> 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
>> primrec factorial :: "nat â 'a"
>> "factorial 0 = 1"
>> | "factorial (Suc n) = of_nat (Suc n) * factorial n"
>> lemma "factorial 3 = 6"
>> by (simp add: eval_nat_numeral)
> 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.
> PGP available:
This archive was generated by a fusion of
Pipermail (Mailman edition) and