Email Gateway (Aug 22 2022 at 11:38): Email Gateway (Aug 22 2022 at 11:38):From: Manuel Eberl <eberlm@in.tum.de>
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.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 11:48):From: Johannes Hölzl <hoelzl@in.tum.de>
For functions like 'fact' and 'exp' it is possible to define it in the
locale of the type class. Here it is welcomed to change.
Unfortunately, for has_derivative this is not possible, as it is defined
between two types.
Email Gateway (Aug 22 2022 at 11:59):From: Makarius <makarius@sketis.net>
(This is an underground part of the thread, resurfaced.)
Which documentation do you mean, "isar-ref" or "locales"? Things can be
only improved when the authors of relevant sections know about it.
Makarius
Last updated: Apr 26 2024 at 01:06 UTC