Stream: math-comp users

Topic: Notation inconsistency : `_.[_ <- _]`


view this post on Zulip Pierre-Yves Strub (Feb 24 2022 at 09:00):

Hi. The notation _.[_ <- _] is not defined with the same priority in PArray (from the Coq standard library) and in finmap. Currently, I have to patch finmap to be able to use both libraries. The fix is pretty straightforward on the finmap side.

view this post on Zulip Pierre Roux (Feb 24 2022 at 09:23):

That seems worth a pull request on finmap.

view this post on Zulip Pierre-Yves Strub (Feb 24 2022 at 13:07):

Pierre Roux said:

That seems worth a pull request on finmap.

https://github.com/math-comp/finmap/pull/95


Last updated: Mar 29 2024 at 11:01 UTC