I've started playing with the exponential in a `realType`

. It is then natural to get the log as the inverse function .

This works well but it seems there is no support to get continuity and differentiability. The file `derive.v`

is a bit scary to me. How should I start if I'd like to add let's say continuity of the inverse function?

Last updated: Jun 22 2024 at 16:02 UTC