[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 MHonArc.