Stream: math-comp users

Topic: Declaring dual structure


view this post on Zulip Evgeniy Moiseenko (Jun 08 2022 at 10:20):

Is there any idiom in mathcomp on how to declare a dual structure, containing all the definitions and lemmas as original one, without just copy-pasting it?

As a concrete example, I need to work with partial orders that have finite ideals:
https://github.com/Event-Structures/event-struct/blob/357797a38c368786717dacb8d88dc4bd247d0a70/theories/common/order.v#L427

Now I want to declare dual structure of partial orders with finite filters.
I want to obtain the same set of definitions and lemmas for the dual structure (modulo renaming s/ideal/filter).


Last updated: Jan 29 2023 at 18:03 UTC