Skip to content

Commit

Permalink
chore: remove CoeFun instances where FunLike is available
Browse files Browse the repository at this point in the history
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

Compared to previous tests, this only preserves the `Finsupp` and `DFinsupp` instances; my guess is that they are the important shortcut instances preventing slowdowns.
  • Loading branch information
Vierkantor committed Oct 21, 2024
1 parent da0c630 commit acdbe3f
Show file tree
Hide file tree
Showing 3 changed files with 0 additions and 14 deletions.
4 changes: 0 additions & 4 deletions Mathlib/Combinatorics/Young/SemistandardTableau.lean
Original file line number Diff line number Diff line change
Expand Up @@ -68,10 +68,6 @@ instance instFunLike {μ : YoungDiagram} : FunLike (SemistandardYoungTableau μ)
cases T'
congr

/-- Helper instance for when there's too many metavariables to apply `CoeFun.coe` directly. -/
instance {μ : YoungDiagram} : CoeFun (SemistandardYoungTableau μ) fun _ ↦ ℕ → ℕ → ℕ :=
inferInstance

@[simp]
theorem to_fun_eq_coe {μ : YoungDiagram} {T : SemistandardYoungTableau μ} :
T.entry = (T : ℕ → ℕ → ℕ) :=
Expand Down
5 changes: 0 additions & 5 deletions Mathlib/Data/DFinsupp/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -81,11 +81,6 @@ instance instDFunLike : DFunLike (Π₀ i, β i) ι β :=
congr
subsingleton ⟩

/-- Helper instance for when there are too many metavariables to apply `DFunLike.coeFunForall`
directly. -/
instance : CoeFun (Π₀ i, β i) fun _ => ∀ i, β i :=
inferInstance

@[simp]
theorem toFun_eq_coe (f : Π₀ i, β i) : f.toFun = f :=
rfl
Expand Down
5 changes: 0 additions & 5 deletions Mathlib/Data/Finsupp/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -116,11 +116,6 @@ instance instFunLike : FunLike (α →₀ M) α M :=
ext a
exact (hf _).trans (hg _).symm⟩

/-- Helper instance for when there are too many metavariables to apply the `DFunLike` instance
directly. -/
instance instCoeFun : CoeFun (α →₀ M) fun _ => α → M :=
inferInstance

@[ext]
theorem ext {f g : α →₀ M} (h : ∀ a, f a = g a) : f = g :=
DFunLike.ext _ _ h
Expand Down

0 comments on commit acdbe3f

Please sign in to comment.