search

math-comp / analysis

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

potential generalization from `realDomainType` to `numDomainType` #696

Open affeldt-aist opened 2 years ago

affeldt-aist commented 2 years ago

https://github.com/math-comp/analysis/blob/d46de60331c7e4ba0f88d31fe11de87484d7b8ed/theories/ereal.v#L2037

https://github.com/math-comp/analysis/blob/d46de60331c7e4ba0f88d31fe11de87484d7b8ed/theories/ereal.v#L2266

https://github.com/math-comp/analysis/blob/d46de60331c7e4ba0f88d31fe11de87484d7b8ed/theories/ereal.v#L2279 (also lee_pmul2l and lee_pmul2r)

CohenCyril commented 2 years ago

Sure, for this kind of change, anything that typechecks!