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".
what's the error message in mathcomp 2.0?
I'd expect it to be the same since predType is not implemented with HB.
Last updated: Oct 13 2024 at 01:02 UTC