## Stream: general

### Topic: simple question

#### Truong Nguyen (Apr 20 2019 at 16:30):

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

and
"
\alpha: Type*
"

#### Truong Nguyen (Apr 20 2019 at 16:35):

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 (Apr 20 2019 at 16:41):

use backtick  A  becomes A

#### Mario Carneiro (Apr 20 2019 at 16:42):

for code snippets use

  lean
bla



#### Mario Carneiro (Apr 20 2019 at 16:44):

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 (Apr 20 2019 at 16:45):

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

#### Kevin Buzzard (Apr 20 2019 at 16:56):

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

#### Truong Nguyen (Apr 22 2019 at 04:00):

 \alpha : Type




#### Truong Nguyen (Apr 22 2019 at 04:01):

\alpha


#### Truong Nguyen (Apr 22 2019 at 04:01):

lean \alpha

#### Truong Nguyen (Apr 22 2019 at 04:02):

 \alpha 

#### Truong Nguyen (Apr 22 2019 at 04:03):

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

#### Keeley Hoek (Apr 22 2019 at 04:04):

Just copy it from vscode

Oh, I see.

#### Truong Nguyen (Apr 22 2019 at 04:05):

\alpha

#### Truong Nguyen (Apr 22 2019 at 04:05):

\forall

#### Greg Conneen (Apr 22 2019 at 11:32):

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 (Apr 22 2019 at 11:40):

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 (Apr 22 2019 at 11:42):

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

#### Keeley Hoek (Apr 22 2019 at 11:44):

Everything should be really speedy after-the-fact!

#### Greg Conneen (Apr 22 2019 at 11:48):

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 (Apr 22 2019 at 11:59):

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 (Apr 22 2019 at 12:00):

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

#### Samuel Lelièvre (Apr 23 2019 at 06:46):

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.

#### Adrian Chu (Apr 24 2019 at 08:55):

what is an emetric space?

#### Kevin Buzzard (Apr 24 2019 at 08:56):

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

#### Kevin Buzzard (Apr 24 2019 at 08:57):

because "e" usually stands for "extended"

#### Kevin Buzzard (Apr 24 2019 at 08:57):

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

#### Kevin Buzzard (Apr 24 2019 at 08:57):

for example ennreal` means "extended non-negative reals"

ok thx

#### Kevin Buzzard (Apr 24 2019 at 08:57):

which is $[0,\infty]$

#### Kevin Buzzard (Apr 24 2019 at 08:58):

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

#### Adrian Chu (Apr 24 2019 at 08:58):

just looking in mathlib, surprised to see gromov hausdorff distance

#### Kevin Buzzard (Apr 24 2019 at 08:59):

mathlib is full of surprises

#### Kevin Buzzard (Apr 24 2019 at 08:59):

That arrived only a few weeks ago IIRC

#### Kevin Buzzard (Apr 24 2019 at 08:59):

Sebastien Gouezel put it there I think

Last updated: May 13 2021 at 06:15 UTC