Oh I see... well... The answer is structures do not compose that way (that's why in Hierarchy Builder (HB) we introduced the command
HB.context). You cannot have a structure and "add stuff". Either you start with "full structures" as in:
Variables (tr : porderType tt) (T : finPOrderType tt). Variables (tr1 : tr) (t1 t2 : T). Check ((tr1, t1) < (tr1, t2))%O.
Or with "naked types" and build your way up like this:
Variables (tr T : Type). Variable tr_choice : Choice.class_of tr. Canonical tr_eqType := EqType tr tr_choice. Canonical tr_choiceType := ChoiceType tr (Choice.mixin tr_choice). Variable tr_o : leOrderMixin [choiceType of tr]. Canonical tr_orderType := POrderType tt tr tr_o. Variable T_fin : Finite.class_of T. Canonical T_eqType := EqType T T_fin. Canonical T_choiceType := ChoiceType T (Choice.mixin T_fin). Canonical T_countType := CountType T T_fin. Canonical T_finType := FinType T T_fin. Variable T_o : leOrderMixin [choiceType of T]. Canonical T_orderType := POrderType tt T T_o. Variables (tr1 : tr) (t1 t2 : T). Check ((tr1, t1) < (tr1, t2))%O.
The later is obviously very tedious and fortunately automated by HB in the future
Léon Ducruet has marked this topic as resolved.
Last updated: Feb 08 2023 at 07:02 UTC