Pierre Jouvelot (Nov 29 2023 at 22:15): Pierre Jouvelot (Nov 29 2023 at 22:15):I'm trying to use a simple ordinal as an orderType (using 8.17 and 1.17). The following attempt fails:
From mathcomp Require Import all_ssreflect all_fingroup.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.Theory.
Open Scope order_scope.
Definition f : forall (T : orderType tt), T -> seq T -> seq T := fun T t0 b => t0 :: b.
Definition x := (@f 'I_2 (@ord0 1) [::]).
What should I be doing instead?
Quentin VERMANDE (Nov 30 2023 at 07:43):The canonical structure is in Order.OrdinalOrder.Exports, so you need to import this module. You will need to generalize the display parameter of orderType (as in f : forall (d : unit) (T : orderType d) ...) since ordinals have their own custom display parameter. Lastly, you may have to leave the implicit arguments of f uninstanciated (it is at least the case with coq 8.15.2 and mathcomp 1.15).
Pierre Roux (Nov 30 2023 at 07:48):Quentin VERMANDE said:
The canonical structure is in
Order.OrdinalOrder.Exports, so you need to import this module.
Given the name, I would have expected the module to be already exported in order.v.
Quentin VERMANDE (Nov 30 2023 at 07:50):On the mathcomp-1 branch, it is (in order.v l.8745), so I am also surprised.
Quentin VERMANDE (Nov 30 2023 at 07:59):Ah, no it works, I did the debugging in the wrong order. Generalizing the display parameter in the definition of f and removing the implicit argument when using it suffices, there is no need to import Order.OrdinalOrder.Exports. Thanks [at]Pierre Roux.
Pierre Jouvelot (Nov 30 2023 at 08:59):Thanks a lot @Quentin VERMANDE @Pierre Roux . For the record, this indeed works:
Definition f : forall (d : unit) (T : orderType d), T -> seq T -> seq T := fun d T t0 b => t0 :: b.
Definition x := (@f _ _ (@ord0 1) [::]). (* or (f (@ord0 1) [::]). *)
Last updated: Oct 13 2024 at 01:02 UTC