Stream: Coq users

Topic: MSets Lemma Cannot Unify.


view this post on Zulip Julia Dijkstra (Jan 09 2024 at 14:23):

Very simple code, but why can

In x (S.elements s) <-> S.In x s

not be proven by applying S.elements_spec1 here?

I have this in my preamble: Module S := Make String_as_OT..

view this post on Zulip Gaëtan Gilbert (Jan 09 2024 at 14:27):

what's the left In? List.In?

view this post on Zulip Julia Dijkstra (Jan 09 2024 at 14:27):

Gaëtan Gilbert said:

what's the left In? List.In?

Yes.

view this post on Zulip Gaëtan Gilbert (Jan 09 2024 at 14:27):

S.In is https://coq.inria.fr/doc/V8.17.1/stdlib/Coq.Lists.SetoidList.html#InA which is different

view this post on Zulip Julia Dijkstra (Jan 09 2024 at 14:40):

Okay that's kind of frustrating :sweat_smile: . It doesn't look like there is a simple equivalence between the two.

view this post on Zulip Gaëtan Gilbert (Jan 09 2024 at 14:50):

there's https://coq.inria.fr/doc/V8.17.1/stdlib/Coq.Lists.SetoidList.html#InA_alt


Last updated: Jun 18 2024 at 22:01 UTC