Stream: math-comp users

Topic: Implement lexical order


view this post on Zulip Léon Ducruet (Jun 22 2022 at 08:15):

Given two partially ordered types T and tr, I would like to implement a lexical order on T * tr. This seems not to be the right way.

From mathcomp Require Import all_ssreflect.

Import DefaultProdLexiOrder.

Section sandbox.

Variable (tr : choiceType).

Variable (T : finType).

Variable tr_o : leOrderMixin tr.

Variable T_o : leOrderMixin T.

Canonical tr_orderType := POrderType Order.lexi_display tr tr_o.

Canonical T_orderType := POrderType Order.lexi_display T T_o.

Variable tr1 : tr.

Variables t1 t2 : T.

Check (((tr1, t1): tr *l T) < ((tr1, t2): tr *l T))%O.

What can I do ? What is missing ?


Last updated: Feb 08 2023 at 07:02 UTC