Notation already defined

Stream: new members

[Kevin Sullivan]

In an old Lean3 file, I'm getting an error, "invalid notation: notation already declared. Consider using 'notation (name := ...)." The use case is super simple, just using /\ to mean "and" in a simple implementation of a simple logic. Has something in the syntax changed lately? Thanks.

notation e1 ∧ e2 :=  pAnd e1 e2

[Kyle Miller]

Yes, it was changed a few months ago to help with the mathport effort. What you can do is

notation (name := something_unique_anything_is_fine) e1 ∧ e2 := pAnd e1 e2

[Kyle Miller]

The name just needs to be different from any other notation that might conflict.

[Kyle Miller]

If there are no such conflicting notations, you can omit the (name := ...)

[Kevin Sullivan]

Kyle Miller said:

If there are no such conflicting notations, you can omit the (name := ...)

So "something_unique" is just a string? Identifier?

[Kyle Miller]

I think it's any identifier. I think the line I gave you should work as-is

[Kyle Miller]

You could do pAnd too if you want to be more principled about it.

[Kevin Sullivan]

Kyle Miller said:

You could do pAnd too if you want to be more principled about it.

Yep, thank you so much. Works. --Kevin