Michael Soegtrop (Feb 01 2022 at 14:30): Michael Soegtrop (Feb 01 2022 at 14:30):@Pierre-Marie Pédrot : as far as I can see there is no Ltac2 integer division, although there is an Division_by_zero exception. Is this a conscious omission or do I miss something?
If we add this, should we add bit operations as well?
Pierre-Marie Pédrot (Feb 01 2022 at 16:56):Please do, I think it has been asked several times already.
Michael Soegtrop (Feb 01 2022 at 18:18):OK, I will do a PR. Do I have to take something special into account to handle the division by zero?
Michael Soegtrop (Feb 07 2022 at 13:28):See PR (https://github.com/coq/coq/pull/15637)
Last updated: Oct 12 2024 at 13:01 UTC