## Stream: Hierarchy Builder devs & users

### Topic: ✔ How should I go with ssralg's linear-like structure?

#### abab9579 (Sep 11 2022 at 12:56):

Hello, I want to build a structure which could also serve as a type, alike `linear` in `math-comp`'s `ssralg`.

Basically, the parts I want is

1. Inheritance hierarchy alike `Additive -> Linear`.
2. `Linear` notation to construct `{linear U -> V}` from the proof that given function is linear.
3. Ability to do `[linear of (f \+ g)]` for `f`, `g` with linear structure.

In addition, I'd like to attach structures, like `zmodType` on an analogue of `{linear U -> V}`.

How do I go with this?

#### Pierre Roux (Sep 11 2022 at 13:56):

Currently, the best solution is to mimic the way `linear` is done in ssralg.v. I admit this is a bit tricky, involving quite a bit of boilerplate.
This should become easier with HB once we release the port https://github.com/math-comp/math-comp/pull/733 , hopefully before christmas.

#### abab9579 (Sep 11 2022 at 14:05):

Sorry, I think I was not being clear. What I want is making a type `CInfty` with notation `{cinfty U -> V}`, and ability to

1. Create a substructure of `CInfty` later
2. `MkCInfty` notation to construct `{cinfty U -> V}` from the proof that given function is C-infinity.
3. Ability to do [cinfty of (f \+ g)] for `f`, `g` with cinfty structure. (C-infinity is also closed in addition)
In addition, I want to attach e.g. `zmodType` on `{cinfty U -> V}`.

`CInfty` would not be substructure of `Linear`, so I do not need to care about internals of `linear`.

#### Pierre Roux (Sep 11 2022 at 14:11):

Sure, but you can take inspiration of how `linear` is done to craft your `CInfty`.

#### abab9579 (Sep 11 2022 at 14:13):

I see what you mean now. Thank you!

#### Notification Bot (Sep 11 2022 at 14:13):

abab9579 has marked this topic as resolved.

Last updated: Aug 03 2024 at 00:02 UTC