[isabelle] Definition of fact
I noticed that âfactâ (the factorail function) is defined as
fun fact :: "nat â ('a::semiring_char_0)"
as opposed to
fun (in semiring_char_0) fact :: "nat â 'a"
where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n"
There are similar issues with some other constants like exp and
has_derivative that make it impossible to use fact/exp/has_derivative
etc. inside type class assumptions.
Is there an actual reason for this? If not, I think this should be changed.
This archive was generated by a fusion of
Pipermail (Mailman edition) and