Nils Buchholz (Feb 06 2024 at 13:17): Nils Buchholz (Feb 06 2024 at 13:17):Is it possible to use both Isabelles F-Division and the euclidean division for Integers in the same theory?
Or would this require redefining one of the two as a separate function?
Manuel Eberl (Feb 09 2024 at 11:21):What is "F-division"?
Nils Buchholz (Feb 11 2024 at 12:32):Division that always rounds down.
So 5/2 = 2 and -5/2 = -3 etc.
Manuel Eberl (Feb 16 2024 at 11:39):That's what Isabelle/HOL's normal div operator already does.
Manuel Eberl (Feb 16 2024 at 11:40):I assume the alternative would be to always round to 0? We don't have one like that, I think. If you want that you'll have to define one yourself and it will be separate from the normal one.
Manuel Eberl (Feb 16 2024 at 11:41):Of course you are then free to introduce whatever kind of notation you want for that operator, e.g. .
Last updated: Apr 28 2024 at 08:19 UTC