simplify vector expressions?

Stream: new members

[Malvin Gattinger]

Is there a tactic to prove things like a = ((a::ᵥ nil).append (c::ᵥ nil)).head without doing it manually?

[Malvin Gattinger]

haha, never mind, refl already works :laughter_tears:

[Alex J. Best]

Does simp also work?

[Malvin Gattinger]

Hmm, but then why does a = ((a::ᵥ b::ᵥ ys).append (c::ᵥ nil)).head not get solved by refl? How can I show that ys really does not matter here?
Edit: okay, cases, refl does it.

[Scott Morrison]

When simp doesn't do something that it obviously should, you should PR the additional @[simp] lemma!

[Scott Morrison]

lemma vector.cons_append_head ...