Typo in documentation for List.all?

Stream: new members

[Kevin Cheung]

In <https://github.com/leanprover/lean4/blob/e9e858a4484905a0bfe97c4f05c3924ead02eed8/src/Init/Data/List/Basic.lean#L1302-L1304>

/--
`O(|l|)`. Returns true if `p` is true for every element of `l`.
* `all p [a, b, c] = p a && p b && p c`

Short-circuits upon encountering the first `false`.
-/
def all : List α → (α → Bool) → Bool
  | [], _ => true
  | h :: t, p => p h && all t p

should the third line say instead `all [a, b, c] p = p a && p b && p c?
From what I see, the type signature has a list as the first argument.

[Philippe Duchon]

The documentation shows the predicate as the first argument, and then the definition shows the list as the first argument. Of course the code has to be right, so the documentation has to be wrong.

If you look at the lines following your example, they use the dot notation with a list as the base type. I suppose this is only possible with the first argument; this in itself looks like a good reason to have the list as the first argument.

[Damiano Testa]

I agree that the doc-string is incorrect.

Btw, dot-notation uses the first explicit[see below] argument of the correct type, not the first argument. This works:

def List.second_arg (n : Unit) (l : List Unit) : List Unit :=
  if n == () then l else l

-- both work
#eval [].second_arg ()
#eval List.second_arg () []

[Philippe Duchon]

Ah, so if several arguments have different types, dot notation could be used for each of them? (so what I said earlier was wrong, making dot notation usable is not a good reason to pick one order over the other)

[Damiano Testa]

I have not tried a situation where multiple dot-notations would apply: I guess that they would have to be nested...

[Damiano Testa]

It looks like dot-notation only works with the "longest possible" type:

def List.New := List

def List.New.two_args (l : List Unit) (m : List.New Unit) : List.New Unit :=
  if l == [] then m else m

def Newnit : List.New Unit := []
def nit : List Unit := []

-- works
#check Newnit.two_args nit

-- error
#check nit.New.two_args Newnit

This is the only example that I tried, so I may well be wrong about this!

[Kyle Miller]

Damiano Testa said:

Btw, dot-notation uses the first explicit argument of the correct type

Correction: it's the first argument of the correct type. What you're saying was true in Lean 3.

[Kyle Miller]

Multiple interpretations of dot notations can't exist — it's the namespace of the declaration that's used for figuring out which argument is used for dot notation. (Though if you use defs to create type synonyms like what Damiano is doing, then you can sometimes get it to use another argument. You can refer to Lean.Elab.Term.typeMatchesBaseName @Damiano Testa)

[Damiano Testa]

Kyle Miller said:

Damiano Testa said:

Btw, dot-notation uses the first explicit argument of the correct type

Correction: it's the first argument of the correct type. What you're saying was true in Lean 3.

Ah, I think that I knew about this, but then I decided it was too weird to be true! :smile:

[Damiano Testa]

docs#Lean.Elab.Term.typeMatchesBaseName does not seem to exist and I can't find something with a similar name eiter...

[Kyle Miller]

It's private — you can find it in Lean/Elab/App.lean

[Damiano Testa]

Very interesting! I had never made it to the source of why "Function" was special.