analysis icon indicating copy to clipboard operation
analysis copied to clipboard
verified publisher icon math-comp

potential generalization from `realDomainType` to `numDomainType`

Open affeldt-aist opened this issue 3 years ago • 2 comments

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)

affeldt-aist avatar Jul 13 '22 00:07 affeldt-aist

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

CohenCyril avatar Oct 07 '22 11:10 CohenCyril