Zulip Chat Archive

Stream: general

Topic: simple question


view this post on Zulip 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*
"

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 20 2019 at 16:41):

use backtick `A` becomes A

view this post on Zulip Mario Carneiro (Apr 20 2019 at 16:42):

for code snippets use

  ```lean
  bla
  ```

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 20 2019 at 16:45):

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

view this post on Zulip Kevin Buzzard (Apr 20 2019 at 16:56):

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

view this post on Zulip Truong Nguyen (Apr 22 2019 at 04:00):

``` \alpha : Type


view this post on Zulip Truong Nguyen (Apr 22 2019 at 04:01):

\alpha

view this post on Zulip Truong Nguyen (Apr 22 2019 at 04:01):

lean \alpha

view this post on Zulip Truong Nguyen (Apr 22 2019 at 04:02):

\alpha

view this post on Zulip 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.

view this post on Zulip Keeley Hoek (Apr 22 2019 at 04:04):

Just copy it from vscode

view this post on Zulip Truong Nguyen (Apr 22 2019 at 04:05):

Oh, I see.

view this post on Zulip Truong Nguyen (Apr 22 2019 at 04:05):

\alpha

view this post on Zulip Truong Nguyen (Apr 22 2019 at 04:05):

\forall

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Greg Conneen (Apr 22 2019 at 11:42):

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

view this post on Zulip Keeley Hoek (Apr 22 2019 at 11:44):

Everything should be really speedy after-the-fact!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 22 2019 at 13:42):

I never compile mathlib -- I download precompiled versions

view this post on Zulip 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.

view this post on Zulip Adrian Chu (Apr 24 2019 at 08:55):

what is an emetric space?

view this post on Zulip Kevin Buzzard (Apr 24 2019 at 08:56):

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

view this post on Zulip Kevin Buzzard (Apr 24 2019 at 08:57):

because "e" usually stands for "extended"

view this post on Zulip Kevin Buzzard (Apr 24 2019 at 08:57):

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

view this post on Zulip Kevin Buzzard (Apr 24 2019 at 08:57):

for example ennreal means "extended non-negative reals"

view this post on Zulip Adrian Chu (Apr 24 2019 at 08:57):

ok thx

view this post on Zulip Kevin Buzzard (Apr 24 2019 at 08:57):

which is [0,][0,\infty]

view this post on Zulip Kevin Buzzard (Apr 24 2019 at 08:58):

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

view this post on Zulip Adrian Chu (Apr 24 2019 at 08:58):

just looking in mathlib, surprised to see gromov hausdorff distance

view this post on Zulip Kevin Buzzard (Apr 24 2019 at 08:59):

mathlib is full of surprises

view this post on Zulip Kevin Buzzard (Apr 24 2019 at 08:59):

That arrived only a few weeks ago IIRC

view this post on Zulip Kevin Buzzard (Apr 24 2019 at 08:59):

Sebastien Gouezel put it there I think


Last updated: May 13 2021 at 06:15 UTC