search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
204 stars 45 forks source link

`conv_gt0` as an instance of `PosNum` #1009

Open affeldt-aist opened 1 year ago

affeldt-aist commented 1 year ago

https://github.com/math-comp/analysis/blob/7880978bcde496d2e638293d165c1654ea17767d/theories/convex.v#L138

"make this an instance of PosNum"

affeldt-aist commented 1 year ago

"I guess you should take inspiration from min and max in signed.v" (@proux01 )