environment already contains '«term⊥»._cstage1' from Mathlib

Stream: new members

[Kevin Sullivan]

Very simple import structure. With either but not both of the last of four imports all is good, but with both of them, this error. One of the imports doesn't import anything and the other imports only Mathlib.Data.Real.Basic. Anyone recognize the problem right off the bat? The full import is Mathlib.Data.Real.Basic.

[Eric Wieser]

Can you make a #mwe?

[Kevin Sullivan]

Eric Wieser said:

Can you make a #mwe?

You may fork this repo: https://github.com/kevinsullivan/cs2120f24.git

[Sebastian Ullrich]

You are redeclaring the mentioned notation that already exists in Mathlib. Try putting it in a namespace.

[Kevin Sullivan]

Sebastian Ullrich said:

You are redeclaring the mentioned notation that already exists in Mathlib. Try putting it in a namespace.

Ay yaiyai. Thx.

[Cody Roux]

While we're at it, is it possible to have this exact comment as the error message?