Notation ::

Stream: general

[Yury G. Kudryashov]

I'm looking at

$ git grep -n 'notation.*:: '
src/data/num/bitwise.lean:196:  notation a :: b := bit a b
src/data/num/bitwise.lean:247:  notation a :: b := bit a b
src/data/sym/basic.lean:76:notation a :: b := cons a b
src/data/sym/basic.lean:129:notation a :: b := cons' a b
src/data/vector3.lean:38:notation a :: b := cons a b
src/number_theory/dioph.lean:257:notation a :: b := cons a b

[Yury G. Kudryashov]

There is also notation a :: b = stream.cons a b and notation a :: b = list.cons a b in Lean core.

[Yury G. Kudryashov]

How does Lean parser choose between these meanings?

[Yury G. Kudryashov]

Should we use something like ::ₘ (used for docs#multiset.cons) more often?

[Yury G. Kudryashov]

#xy I'm moving docs#stream from core to mathlib. Should I change notation for docs#stream.cons? Move it (and other notation about stream) to a locale?

[Kyle Miller]

(I've been meaning to replace data/sym/basics notation. It managed to avoid getting its own right around when @Johan Commelin modified the multiset notation.)

[Kyle Miller]

How it seems to work is that Lean takes all the possible alternatives and checks to see which ones might actually apply based on types, and if there are multiple possibilities in the end, it fails with an error. I've never really understood exactly when this occurs...

[Kyle Miller]

This is something within its capabilities for example:

notation `🌴` := (37 : ℕ)
notation `🌴` := (37 : ℤ)

example : ℕ := 🌴
example : ℤ := 🌴

[Johan Commelin]

Should there be a has_cons class?

[Yury G. Kudryashov]

In most cases has_cons (α : out_param (Type u)) (β : Type v) := (cons : α → β → β) will work but it will fail for docs#vector and docs#sym. What should be the signature?

[Johan Commelin]

Hmm, I see. Maybe those two can use their own subscripted notation?

[Gabriel Ebner]

What Kyle said is accurate, Lean tries all specified overloads and fails if they are ambiguous.

[Gabriel Ebner]

For now in Lean 3, I'd suggest to have different notations for every cons.