Zulip Chat Archive

Stream: general

Topic: What is `import standard`?


Eric Wieser (Jan 25 2021 at 18:20):

#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 (Jan 25 2021 at 19:09):

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

Bryan Gin-ge Chen (Jan 25 2021 at 19:53):

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 (Jan 26 2021 at 13:32):

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


Last updated: Dec 20 2023 at 11:08 UTC