search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
201 stars 44 forks source link

Wrong documentation? #1038

Closed affeldt-aist closed 4 weeks ago

affeldt-aist commented 1 year ago

https://github.com/math-comp/analysis/blob/a5e2c659ea31a86b4789c9094f771d960187bf5c/theories/realfun.v#L14-L15

@CohenCyril I remember that you recently made a comment about this documentation being wrong but I cannot find your comment. What was it?

CohenCyril commented 1 year ago

cf https://github.com/math-comp/analysis/pull/873#discussion_r1296858851 and https://github.com/math-comp/analysis/pull/794#discussion_r1038602313