has been declared

Stream: lean4

[Young]

What happened if Lean infoview tells me "has been declared"?

For example,
error: .\.\.\.\Mathlib\Data\List\Defs.lean:492:4: 'List.finRange' has already been declared
( I've tried to "lake update" and it succeed)

[Daniel Weber]

Could you give some context? List.finRange has been recently moved from Mathlib to Batteries, so its possible your versions of them are mismatched

[Young]

I think "lake update" may solve the problem. Maybe I should "downdate"?

[Young]

✖ [665/1427] Building Mathlib.Data.List.Defs
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake/packages\LeanSearchClient\.lake\build\lib;.\.\.lake/packages\plausible\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\A1exa\.elan\toolchains\leanprover--lean4---v4.14.0-rc2\bin\lean.exe -Dpp.unicode.fun=true -DautoImplicit=false -Dweak.linter.docPrime=true -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.header=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.multiGoal=true -Dweak.linter.style.setOption=true .\.\.\.\Mathlib\Data\List\Defs.lean -R .\.\.\. -o .\.\.lake\build\lib\Mathlib\Data\List\Defs.olean -i .\.\.lake\build\lib\Mathlib\Data\List\Defs.ilean -c .\.\.lake\build\ir\Mathlib\Data\List\Defs.c --json
error: .\.\.\.\Mathlib\Data\List\Defs.lean:492:4: 'List.finRange' has already been declared
error: Lean exited with code 1

[Young]

⚠ [41/1427] Replayed Mathlib.Tactic.Simps.NotationClass
warning: .\.\.\.\Mathlib\Tactic\Simps\NotationClass.lean:51:15: Lean.Expr.forallArity has been deprecated, use Lean.Expr.getNumHeadForalls instead
warning: .\.\.\.\Mathlib\Tactic\Simps\NotationClass.lean:85:15: Lean.Expr.forallArity has been deprecated, use Lean.Expr.getNumHeadForalls instead

[Young]

I've tried to delete List.finRange in Mathlib

[Ruben Van de Velde]

How did you get into this situation? Are you in mathlib itself or in a project that depends on mathlib?

[Ruben Van de Velde]

If the latter, what do you lake file and lake manifest look like?