What is `import standard`?

Stream: general

[Eric Wieser]

#naming contains imports like import standard algebra.ordered_ring. Lean tells me "invalid import: standard".

Did there used to be a standard module? Do the code examples need updating on that page?

[Reid Barton]

The check without # makes me think this is Lean 2 or something

[Bryan Gin-ge Chen]

Feel free to make a PR removing that, though I don't know whether it's worth the effort to keep all the code examples there runnable, given how fast mathlib changes.

Maybe if someone designs a "literate Lean" format we could run CI on these...

[Eric Wieser]

leanprover-community/leanprover-community.github.io#163