analysis icon indicating copy to clipboard operation
analysis copied to clipboard

Published 20 hours ago • verified publisher icon math-comp

Use instance of realType once we get one

Open proux01 opened this issue 4 months ago • 0 comments

In theories/normedtype.v

(* Ideally, R should be an instance of realType here,                                                            
   rather than a section variable. *)

C.f. https://github.com/math-comp/analysis/pull/1347

proux01 avatar Oct 15 '24 11:10 proux01