I defined my own Order module (loosely based on the Ordinal one), and wanted to write some generic functions dedicated to maximums. Is there a way to make the last definition below typecheck?
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.Theory.
Local Open Scope order_scope.
Variable (k : nat) (T : tbLatticeType tt) (t0 : T).
Lemma foo (t : k.+1.-tuple T) : (tnth t ord0 = t0)%O.
Admitted.
Lemma bar (t : k.+1.-tuple T) : (\max_(i < k.+1) tnth t i = t0)%O.
I tried to use other domains (orderType, ...), but couldn't find a way to make this work. What am I doing wrong?
It seems the only big operators that are defined in order.v
are \join
and \meet
. I think you should use \join
Last updated: Oct 13 2024 at 01:02 UTC