search

math-comp / mcb

Mathematical Components (the Book)
Other
140 stars 25 forks source link

intended meeting? #120

Closed marklemay closed 3 years ago

ybertot commented 3 years ago

Did you want the title to be "intended meaning?"

ybertot commented 3 years ago

Just doing statistics in the math-comp library itself, we see that idP is used on 1044 lines, and on the same line as iffP on 186 lines. That's about 1/6 of the time. If we perform the same test in math-comp/odd-order, then the numbers are 518 uses of idP, for only 8 uses in conjunction with iffP (1.5%). In math-comp/analysis, it's half the time: 87 uses of idP, for 41 uses in conjunction with iffP.

When I started these tests, I thought "often" was too strong, but starting at 1/6, I think it is adequate. I am not the initial author of this line, but I approve the change.

gares commented 3 years ago

Thanks