Panic at `Lean.AsyncConsts.add`

Stream: lean4

[Tomas Skrivan]

While bumping SciLean from v4.16.0 to v4.18.0 I encountered strange panic

PANIC at _private.Lean.Environment.0.Lean.AsyncConsts.add Lean.Environment:444:4: AsyncConsts.add: duplicate normalized declaration name StateT.bind.match_1.eq_1 vs. _private.SciLean.Analysis.Calculus.Monad.StateT.0.StateT.bind.match_1.eq_1

Unfortunately I can't minimize it, it happens on this instance. The issue is simp[StateT.bind.match_1], if remove it it works again.

Is explicitly unfolding match statements with simp is now bad/problematic?

[Sebastian Ullrich]

A minimization really would be helpful :)

[Tomas Skrivan]

Yeah I understand, I will try to minimize it