Stream: Beginner Questions

Topic: ✔ to_nat (from_nat x) = x

Manuel Eberl (Oct 21 2022 at 16:39):

It generally has some nicer properties. It would make sense to define to_nat in terms of to_nat_on and inherit all the nice properties.

Robert Soeldner (Oct 21 2022 at 17:18):

great answer, thank you

Notification Bot (Oct 21 2022 at 17:18):

Robert Soeldner has marked this topic as resolved.

Last updated: Nov 13 2025 at 08:29 UTC