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
\meet. I think you should use
Last updated: Feb 08 2023 at 07:02 UTC