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: May 28 2023 at 18:29 UTC