Jakub Kądziołka (Jan 28 2021 at 13:25): Jakub Kądziołka (Jan 28 2021 at 13:25):I have a 'a::{factorial_semiring, comm_ring}. I would like to derive the semiring_modulo class for it, by defining a mod b = a - a div b. Is this possible?
Manuel Eberl (Jan 28 2021 at 13:32):Not generically, no. But you can probably do it for a particular instance.
Manuel Eberl (Jan 28 2021 at 13:33):Our of curiosity, what type is it that you have?
Jakub Kądziołka (Jan 28 2021 at 13:48):I just want to prove some theorems for an arbitrary UFD
Manuel Eberl (Jan 28 2021 at 14:57):Yeah then you probably have to assume a type class that has modulo if you want modulo to be available.
Manuel Eberl (Jan 28 2021 at 14:57):The only other way I can think of is to define a type 'a ufdmod that is basically a copy of 'a except that it also has a modulo operation defined the way you just said.
Manuel Eberl (Jan 28 2021 at 14:58):Then you can pull all the results that don't use mod over from 'a ufdmod to 'a using e.g. the transfer tool.
Manuel Eberl (Jan 28 2021 at 14:58):Might not be worth it though.
Manuel Eberl (Jan 28 2021 at 14:58):Might be easier to just not use mod.
Manuel Eberl (Jan 28 2021 at 14:59):What you could also do is interpret the semiring_modulo locale with that particular definition of mod.
Manuel Eberl (Jan 28 2021 at 14:59):I've done that sort of thing before. It's a little bit messy, but it does the job.
Last updated: Dec 21 2024 at 16:20 UTC