Zulip Chat Archive
Stream: general
Topic: simp list.map id
Sean Leather (Sep 28 2018 at 08:58):
Interesting that simp doesn't solve list.map (λ t, t) l = l.
Sean Leather (Sep 28 2018 at 08:59):
I suppose I could add this to the simp:
theorem map_id' {f : α → α} (h : ∀ x, f x = x) (l : list α) : map f l = l
Sean Leather (Sep 28 2018 at 09:00):
Yep, simp [list.map_id'] does the job.
Last updated: Dec 20 2023 at 11:08 UTC