How to make a decidable instance computable?

Stream: new members

[Vivek Rajesh Joshi]

def Vector.Mem (a : α) : Vector α n → Prop := fun v => v.toList.Mem a

instance : Membership α (Vector α n) where
  mem := Vector.Mem

theorem Vector.mem_def (v : Vector α n) : a ∈ v ↔ a ∈ v.toList := Iff.rfl

instance (a : α) (v : Vector α n) : Decidable (a ∈ v) := by
  rw [Vector.mem_def]
  if ha : a ∈ v.toList then exact .isTrue ha else exact .isFalse ha

Is there a way to make the instance for Decidable (a \in v) computable?

[Kyle Miller]

instance [DecidableEq α] (a : α) (v : Vector α n) : Decidable (a ∈ v) :=
  inferInstanceAs <| Decidable (a ∈ v.toList)

[Vivek Rajesh Joshi]

Thanks. Could you please explain to me how exactly InferInstanceAs works?

[Kyle Miller]

Have you looked at its definition yet? It's a plain function. inferInstanceAs

In case <| isn't familiar, this is equivalent to putting down a ( and then a ) as late as possible. So, in this case, inferInstanceAs (Decidable (a ∈ v.toList)).