We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 6cd948c commit d762d16Copy full SHA for d762d16
1 file changed
Mathlib/ModelTheory/LanguageMap.lean
@@ -505,7 +505,7 @@ variable {L} (A) {N : Type w'} [L.Structure N] (f : M ↪[L] N)
505
/-- Type synonym for `N` used to equip it with an `L[[A]]`-structure where the new constants on `A`
506
are interpreted via the embedding `f`. -/
507
@[nolint unusedArguments]
508
-def Embedding.withConstants (f : M ↪[L] N) (A : Set M) : Type w' := N
+def Embedding.withConstants (_f : M ↪[L] N) (_A : Set M) : Type w' := N
509
510
instance : L.Structure (f.withConstants A) := by
511
dsimp [Embedding.withConstants]
0 commit comments