Documentation typos #474
Documentation typos #474
Conversation
|
For me, this PR can be merged as it is. (Thanks @llelf .) |
mathcomp/ssreflect/tuple.v
Outdated
| (* [tuple E | i < n] == the n.-tuple with general term E (i : 'I_n is bound *) | ||
| (* in E). *) | ||
| (* tcast Emn t == the m-tuple t cast as an n-tuple using Emn : m = n. *) | ||
| (* tcast Emn t == the m.-tuple t cast as an n-tuple using Emn : m = n. *) |
There was a problem hiding this comment.
I disagree with this modification. I don't see why adding a period here will help. Can you elaborate the need for this change?
There was a problem hiding this comment.
For consistency. foo.-tuple (as a notation for tuple_of) is used everywhere in this file's header.
There was a problem hiding this comment.
it should be even the m.-tuple t cast as an n.-tuple then.
@ybertot apply or remove?
There was a problem hiding this comment.
@llelf You convinced me, and you are right about the second correction on the same line: --> "n.tuple"
There was a problem hiding this comment.
So I propose to fix L.16: (size s)-tuple -> (size s).-tuple.
the->this Co-Authored-By: Yves Bertot <yves.bertot@inria.fr>
|
Thanks a lot @llelf, it was great working with you on this pull request. |
4 participants
No description provided.