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

num_normedtype.v imported HB but doesn't use

Open IshiguroYoshihiro opened this issue 7 months ago • 0 comments

https://github.com/math-comp/analysis/blob/05898dcecc81e696b04dde8883718d54f2109990/theories/normedtype_theory/num_normedtype.v#L2

num_normedtype.v improted HB, but does not use HB.

IshiguroYoshihiro avatar May 21 '25 11:05 IshiguroYoshihiro