anonymous constructor inconsistency

Stream: lean4

[Yuri de Wit]

I noticed that this works:

#check { fst := 1, snd := "aa" : Prod Nat String } -- works

But this does not work:

#check ⟨ 1, "aa" : Prod Nat String ⟩ -- error: expected '⟩'

A tiny inconsistency, it seems.

[Alex Keizer]

You can get the same effect by using a type ascription outside the magic brackets

#check (⟨ 1, "aa" ⟩ : Prod Nat String)

Or, if you really want the type inside, a simple macro fixes that

macro "⟨" a:term ", " b:term ":" t:term "⟩" : term => `((⟨$a:term, $b:term⟩ : $t:term))

[Yuri de Wit]

Thank you!

Where should these be reported? Reporting these in the Lean4 github is the obvious place, but it is my understand that the Lean4 devs prefer that we avoid creating issues in the lean4 github repo for now.

[Alex Keizer]

I don't think this warants reporting, per se? In any case, the devs actually monitor this chat quite closely. You could ping one of them directly, if you really feel that strong about it

[Yuri de Wit]

I guess it is debatable, but to me consistency is something that one needs to strive for even if this is very low priority item.

I think the main point is that we need a place where we can report these issues however important they are. It either gets queued up for later, for contributions or even closed with a simple justification so that no one else needs to wonder about it or asks the same question again.