dsimp failing

Stream: general

[Kevin Buzzard]

example (A : Type) (a : list A) (L : list (list A)) :
  list.join (a :: L) = a ++ list.join L := by dsimp -- fails

rfl works. Does this mean that this example has not been tagged with [simp]? I don't even know if this theorem has a name -- library_search tells me the proof is exact rfl. I couldn't get #find to give any output at all:

import tactic.find

def find_bug_workaround := 37

#find list.join (_ :: _) = _ ++ list.join _

variables (A : Type) (a : list A) (L : list (list A))

#find list.join (a :: L) = a ++ list.join L

Is it a bad simp lemma?

[Scott Morrison]

Sounds like a good simp lemma to me!

[Simon Hudon]

Maybe we should tag list.join with @[simp]

[Scott Morrison]

Yes.