Stream: Hierarchy Builder devs & users

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

view this post on Zulip 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?

view this post on Zulip 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.

Last updated: Jan 29 2023 at 15:02 UTC