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

- Inheritance hierarchy alike
`Additive -> Linear`

. `Linear`

notation to construct`{linear U -> V}`

from the proof that given function is linear.- 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?

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.

Sorry, I think I was not being clear. What I want is making a type `CInfty`

with notation `{cinfty U -> V}`

, and ability to

- Create a substructure of
`CInfty`

later `MkCInfty`

notation to construct`{cinfty U -> V}`

from the proof that given function is C-infinity.- 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`

.

Sure, but you can take inspiration of how `linear`

is done to craft your `CInfty`

.

I see what you mean now. Thank you!

abab9579 has marked this topic as resolved.

Last updated: May 28 2023 at 18:29 UTC