Stream: math-comp users

Topic: Stuck with list membership

view this post on Zulip Yves Bertot (Apr 26 2023 at 07:27):

I just defined a new type, exhibited a boolean equality function, proved the reflection lemma, and forgot to set the canonical structure. I then try to write a formula with list membership, and got an obscure error message. I wish we can improve the error message:

   fun (x : my_type) (l : seq my_type) => x \in l
In environment
R : realType
x : vert_edge
l : seq vert_edge
The term "l" has type "seq vert_edge" while it is expected to have type
 "pred_sort ?pT".

view this post on Zulip Cyril Cohen (Apr 26 2023 at 08:14):

what's the error message in mathcomp 2.0?

view this post on Zulip Pierre Roux (Apr 26 2023 at 08:22):

I'd expect it to be the same since predType is not implemented with HB.

Last updated: Jul 15 2024 at 20:02 UTC