simple question

Stream: general

[Truong Nguyen]

Can you tell me what is the different when we type:
"
universe u
\alpha : Type u
"

and
"
\alpha: Type*
"

[Truong Nguyen]

By the way,
I don't know how other people can create alpha symbol in chat message, it appears similarly VS code editor.

Can you tell me the way to write the code that appear as in VS code editor?

[Mario Carneiro]

use backtick `A` becomes A

[Mario Carneiro]

for code snippets use

  ```lean
  bla
  ```

[Mario Carneiro]

There is almost no difference between

universe u
variable α : Type u

and

variable α : Type*

In the first case you give a name to the universe variable so you can refer to it, in the second it is anonymous

[Mario Carneiro]

there is no magic sauce for producing a α on chat, I copy paste from vscode

[Kevin Buzzard]

Can we have this magic sauce please? I am getting sick of copy pasting from vscode

[Truong Nguyen]

``` \alpha : Type

[Truong Nguyen]

\alpha

[Truong Nguyen]

lean \alpha

[Truong Nguyen]

\alpha

[Truong Nguyen]

Hi, every one,
I am trying to type Greek letter in the message, but I did not manage it.

[Keeley Hoek]

Just copy it from vscode

[Truong Nguyen]

Oh, I see.

[Truong Nguyen]

\alpha

[Truong Nguyen]

\forall

[Greg Conneen]

Do people generally use VSCode for Lean? I do, since it was recommended by my professor, and I like the extension. But sometimes it takes a while to import documents and resolve proof tactics when my file is pretty long. Is this a common issue?

[Keeley Hoek]

Greg, you should pre-compile your project with leanpkg build at the command line while in the directory of your project---that way the whole thing won't have to recompile every time you start a new session. If you use mathlib, you can also from the root directory of your project do lean --make _target/mathlib to pre-compile the whole of mathilib, which will take ages, but will be worth it if you use it often (the previous command only compiles the pieces of mathlib which your project currently uses)

[Greg Conneen]

Ah, I see. I do use mathlib, so this is very useful.

[Keeley Hoek]

Everything should be really speedy after-the-fact!

[Greg Conneen]

I got the error "failed to start child process." I assume that has to do with how I've set up my folders? I'm not familiar with Windows, as before I started needing Windows-exclusive software I was only using Linux. How would I go about fixing this?

[Keeley Hoek]

Ah, I think this is due to how you are invoking your copy oflean---there is not very good support currently for leanpkg on windows. Instead, you have to be inside a unix-emulated shell, e.g. git for windows, or msys2. My suggestion regarding the direct lean --make should still work though I think

[Greg Conneen]

okay, great. That's really annoying, but at least --make is still usable. Thank you so much.

[Kevin Buzzard]

I never compile mathlib -- I download precompiled versions

[Samuel Lelièvre]

I am getting sick of copy pasting from vscode

Some browser add-ons let you use an external text editor to type in text fields on web pages.

• GhostText: https://github.com/GhostText/GhostText

[Adrian Chu]

what is an emetric space?

[Kevin Buzzard]

so let me say that I don't know, but I can guess

[Kevin Buzzard]

because "e" usually stands for "extended"

[Kevin Buzzard]

and in the context of the real numbers this usually means "add +infinity or +-infinity"

[Kevin Buzzard]

for example ennreal means "extended non-negative reals"

[Adrian Chu]

ok thx

[Kevin Buzzard]

which is $[0,\infty]$

[Kevin Buzzard]

so my guess is that an emetric space allows $d(x,y)=+\infty$

[Adrian Chu]

just looking in mathlib, surprised to see gromov hausdorff distance

[Kevin Buzzard]

mathlib is full of surprises

[Kevin Buzzard]

That arrived only a few weeks ago IIRC

[Kevin Buzzard]

Sebastien Gouezel put it there I think