Glitch in lean4 doc string for List

Stream: lean4

[Hunter Monroe]

This looks like a glitch in the doc strings of Init.Data.List in Basic.lean where it has O(|l|). You see this in any lean file if you hover over List.erase to see the doc string. No other lean file has the string O(.

`O(|l|)`. `erase l a` removes the first occurrence of `a` from `l`.

[Kim Morrison]

@Hunter Monroe, what do you think is the glitch? I'm not sure what you think is wrong here.

[Hunter Monroe]

What is O(|l|)? Is it big O notation for the time required to compute the List.erase function? For eraseDups, the doc string begins O(|l|^2), and that function requires a loop within a loop.

[Hunter Monroe]

Actually the doc string for List.append says "It takes time proportional to the first list." so it must be big O notation.

[Hunter Monroe]

I put #check List.append in a .lean file and wondered why the tooltip was giving big O notation.

[Kim Morrison]

Yes, it's describing the runtime of the function. If you'd like to make a PR rearranging the comment so the runtime description comes later, and is more clearly about runtime, I will merge it! :-)

[Mario Carneiro]

This is a pattern borrowed from the std docs which use it more heavily

[Mario Carneiro]

I think it is good to have information in the docstring be sorted from more compact to less compact so that skimming works