docstring for IO

Stream: lean4

[Kevin Buzzard]

I've never really looked at the reference manual, but I just ran into it in an open tab and thought I'd give it a go. In "Introduction" we have a preliminary section on history, and then we see our first line of Lean code, powered by Verso, in 1.2.1. Lean Code and it's def hello : IO Unit := .... I hover over Unit and get a lovely docstring; I hover over IO and it just says IO : Type → Type. This might be the first Lean code that people ever see (if they stumble on the language via the reference manual) -- isn't this good motivation to just slap a quick docstring on IO and IO.println, the other function which we get to see in action in this very first line of code in the book? I would make a PR myself but I don't have the first clue what IO is (other than "it's a monad and has something to do with programming") (but I would maybe know more if there were a docstring!).

[Sebastian Ullrich]

Thanks for checking, I think you're just a few days early: lean#7476

[Kevin Buzzard]

Oh amazing! Carefully documenting the entire IO.lean file is indeed the correct solution!