Zulip Chat Archive

Stream: new members

Topic: vector mem


view this post on Zulip Horatiu Cheval (Mar 11 2021 at 12:59):

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?

view this post on Zulip Anne Baanen (Mar 11 2021 at 13:05):

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

view this post on Zulip Anne Baanen (Mar 11 2021 at 13:07):

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

view this post on Zulip Anne Baanen (Mar 11 2021 at 13:07):

So you would have to write:

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

view this post on Zulip Horatiu Cheval (Mar 11 2021 at 13:13):

Thanks!


Last updated: May 14 2021 at 00:42 UTC