vector mem

Stream: new members

[Horatiu Cheval]

How can I write a ∈ t with a : α and t : vector α n? Should I define myself a has_mem instance for vector or can I somehow use the instance for list, since vector is a subtype of it?

[Anne Baanen]

Both ways would work, either define the has_mem α (vector α n) instance, or write a ∈ (t : list α).

[Anne Baanen]

Hmm, there isn't a coercion from vector to list, apparently.

[Anne Baanen]

So you would have to write:

example {α : Type*} {n : ℕ} (a : α) (t : vector α n) : Prop := a ∈ t.1

[Horatiu Cheval]

Thanks!