Stream: math-comp users

Topic: \max with order.v


view this post on Zulip Pierre Jouvelot (May 09 2022 at 13:35):

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?

view this post on Zulip Laurent Théry (May 09 2022 at 14:30):

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