deprecation message

Stream: new members

[Darij Grinberg]

Quick question... VSCode says

gt_of_ge_of_gt has been deprecated: use lt_of_le_of_lt' instead

Shouldn't it be "lt_of_lt_of_le"

[Kenny Lau]

image.png

image.png

[Kenny Lau]

image.png

[Kenny Lau]

Darij Grinberg said:

Quick question... VSCode says

gt_of_ge_of_gt has been deprecated: use lt_of_le_of_lt' instead

Shouldn't it be "lt_of_lt_of_le"

no, the order of the "of_X" follows the order you see on your screen

[Kenny Lau]

the first part is the conclusion

[Kenny Lau]

to be clear, A_of_B_of_C means B -> C -> A

[Kenny Lau]

the conclusion goes first, and then each assumption from left to right

[Darij Grinberg]

oooh there is a ' there that i missed
thanks!

[Kenny Lau]

the ' has no difference, in fact I think the version with ' should be removed, it's entirely identical

[Kenny Lau]

oh wait

[Kenny Lau]

nvm the order is different