Open IshiguroYoshihiro opened 1 month ago
I found some lemmas about GRing.opp which is named opp_ ... or ... _opp, not oppr_ ... or ... _oppr. I suppose these may be for distinguish between GRing.opp for number and for function, but it bothers me a little. For instance, opp_continuous in normedtype.v. https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/theories/normedtype.v#L2399 As there is also a oppe_continuous, I think that it is appropriate to name it as oppr_continuous. https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/theories/ereal.v#L892-L893
GRing.opp
opp_ ...
... _opp
oppr_ ...
... _oppr
opp_continuous
normedtype.v
oppe_continuous
oppr_continuous
the followings are some of other, https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/classical/set_interval.v#L453-L454 https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/theories/realfun.v#L1960-L1962
I found some lemmas about
GRing.oppwhich is namedopp_ ...or... _opp, notoppr_ ...or... _oppr. I suppose these may be for distinguish betweenGRing.oppfor number and for function, but it bothers me a little. For instance,opp_continuousinnormedtype.v. https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/theories/normedtype.v#L2399 As there is also aoppe_continuous, I think that it is appropriate to name it asoppr_continuous. https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/theories/ereal.v#L892-L893the followings are some of other, https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/classical/set_interval.v#L453-L454 https://github.com/math-comp/analysis/blob/99c3a8336d2ca461f2766d18293cd26cbe4b1069/theories/realfun.v#L1960-L1962