definition for Hilbert Space

Stream: mathlib4

[Mingyuan Zhang]

Hello guys! I'm new to Lean4, and currently there is something that looks weird to me: In Mathlib.Analysis.InnerProductSpace.Defs (line: 593 - 596), one defines the HilbertSpace as a Type

structure HilbertSpace (𝕜 E : Type*) [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]

Why is it preferred to define the HilbertSpace as a Type instead of a Type Class? I don't really get this point :sob: Help :(

[Moritz Doll]

There was a discussion about this: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Is.20there.20code.20for.20Hilbert.20Spaces.3F/with/510364826
I guess however that Sebastien's point still stands: it might be easier to just use
variable [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace RC E]