Skip to content

Commit

Permalink
chore(Data/List): make List.map_const' be simp (#17622)
Browse files Browse the repository at this point in the history
`List.map_const` is already simp but stated using `Function.const` rather than a plain lambda, so it never fires in my application.

From LeanCamCombi
  • Loading branch information
YaelDillies committed Oct 11, 2024
1 parent fe48a46 commit 7a7d5c0
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions Mathlib/Data/List/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -887,6 +887,11 @@ theorem get_set_of_ne {l : List α} {i j : ℕ} (h : i ≠ j) (a : α)

/-! ### map -/

-- `List.map_const` (the version with `Function.const` instead of a lambda) is already tagged
-- `simp` in Core
-- TODO: Upstream the tagging to Core?
attribute [simp] map_const'

@[deprecated (since := "2024-06-21")] alias map_congr := map_congr_left

theorem bind_pure_eq_map (f : α → β) (l : List α) : l.bind (pure ∘ f) = map f l :=
Expand Down

0 comments on commit 7a7d5c0

Please sign in to comment.