Sophie Tourret (Oct 13 2022 at 07:39): Sophie Tourret (Oct 13 2022 at 07:39):@Mathias Fleury: What I expected was to declare the subclass and provide just below the definitions of < and ≤, following what is shown in the type classes documentation. I was hoping there would be a way to turn off or rename one of the dependencies, as can be done for notations when there is a conflict.
Now I get this is just not possible, and I know of two ways to go around this kind of problem in the future, so thanks @Mathias Fleury and @Manuel Eberl for the detailed answers!
Notification Bot (Oct 13 2022 at 07:39):Sophie Tourret has marked this topic as resolved.
Last updated: Dec 21 2024 at 16:20 UTC