Stream: Ltac2

Topic: Ltac2 integer operations


view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Feb 01 2022 at 16:56):

Please do, I think it has been asked several times already.

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Feb 07 2022 at 13:28):

See PR (https://github.com/coq/coq/pull/15637)


Last updated: Jan 31 2023 at 10:01 UTC