Zulip Chat Archive

Stream: new members

Topic: How do I import metric space in Lean Web Editor

view this post on Zulip Lars Ericson (Dec 02 2020 at 04:17):

I am using Lean Web Editor: https://leanprover-community.github.io/lean-web-editor/#

I would like to import metric_space.

Lean Web Editor doesn't seem to know mathlib, in the sense that none of these work:

import topology
import topology.metric_space
import topology.metric_space.basic

All result in the error

file 'topology' not found in the search path
invalid import: topology
could not resolve import: topology

Is there a way to point Lean Web Editor to mathlib?

view this post on Zulip Lars Ericson (Dec 02 2020 at 04:29):

Never mind, I figured it out after installing the local editor from this video: https://youtu.be/02ff4WrW0FU

import topology.metric_space.basic

It is a lot easier to use the local editor because it tells you as you're typing what is available. I'm going local from now on!

view this post on Zulip Kenny Lau (Dec 02 2020 at 04:31):

wise choice

view this post on Zulip Bryan Gin-ge Chen (Dec 02 2020 at 04:58):

For what it's worth, the topology.metric_space.basic import does work for me on the web editor, see here. But yes, the local editor is much, much better!

Last updated: May 11 2021 at 13:22 UTC