Zulip Chat Archive

Stream: general

Topic: Are these tokens?

Kevin Buzzard (Apr 01 2018 at 19:44):

In VS Code, if I type #check nat.and then, with the cursor just to the right of the . I type Esc then ctrl-space (possibly more than once) then I get, I think, to see a list of things which the Lean VS Code plugin thinks might come next. In this particular case, the list seems to naturally split into two types of things.

Kevin Buzzard (Apr 01 2018 at 19:44):

The first type of thing is the "purple cube" type of thing, which are all the possibilities which are prefixed by a little drawing of a purple hexagon/cube thing.

Kevin Buzzard (Apr 01 2018 at 19:45):

In this particular case they seem to be every single theorem / definition / constructor etc (perhaps every single name?) which starts nat.X where X begins with a, b, c or d.

Kevin Buzzard (Apr 01 2018 at 19:45):

The fact that it stops at d might be a bug in the VS Code Lean plugin.

Kevin Buzzard (Apr 01 2018 at 19:46):

But, from nat.add to nat.discriminate they're all "purple cube" choices.

Kevin Buzzard (Apr 01 2018 at 19:47):

And then after the purple cube choices, we have the "about 7 straight lines" choices

Kenny Lau (Apr 01 2018 at 19:47):

The fact that it stops at d might be a bug in the VS Code Lean plugin.

or maybe because there are too many possibilities?

Kevin Buzzard (Apr 01 2018 at 19:49):

The "7 straight lines" possibilities start #check #compile #eval #exit #help #print #reduce #unify

Kevin Buzzard (Apr 01 2018 at 19:50):

and then there's a whole bunch more, add_key_equivalence assume at attribute axiom axioms begin by calc class coinductive...

Kevin Buzzard (Apr 01 2018 at 19:50):

there is def but no definition

Kenny Lau (Apr 01 2018 at 19:51):

wait, coinductive?

Kevin Buzzard (Apr 01 2018 at 19:51):

there is theorem though.

Kenny Lau (Apr 01 2018 at 19:51):

wait, I thought we don't have coinductive!

Kevin Buzzard (Apr 01 2018 at 19:51):

VS Code says it's there

Kevin Buzzard (Apr 01 2018 at 19:51):

but then again I thought we had definitions

Kevin Buzzard (Apr 01 2018 at 19:51):

and VS Code says no

Kenny Lau (Apr 01 2018 at 19:52):

nah, coinductive hasn't been implemented

Kevin Buzzard (Apr 01 2018 at 19:52):

These are strange choices for completions because nat.theorem makes no sense

Kevin Buzzard (Apr 01 2018 at 19:52):

vm check failed: is_closure(o) (possibly due to incorrect axioms, or sorry)

Kevin Buzzard (Apr 01 2018 at 19:52):

I think you get an achievement for that error

Kevin Buzzard (Apr 01 2018 at 19:53):

I'll give you an octopus

Kenny Lau (Apr 01 2018 at 19:53):

thanks

Kevin Buzzard (Apr 01 2018 at 19:54):

So are these "7 straight lines" almost the complete list of symbols and commands?

Kevin Buzzard (Apr 01 2018 at 19:54):

except that they do mention coinductive and don't mention definition...

Kevin Buzzard (Apr 01 2018 at 19:56):

As well as "purple cube" and "7 lines" I can get "abc in a box"

Kevin Buzzard (Apr 01 2018 at 19:56):

which might mean "string"

Kevin Buzzard (Apr 01 2018 at 19:58):

although ctrl-space after #check "abc"gives me that #check is an abc-in-a-box

Kevin Buzzard (Apr 01 2018 at 19:59):

Maybe purple cube means "identifier"

Kevin Buzzard (Apr 01 2018 at 20:08):

Reading through the docs of Lean VS Code extension doesn't seem to mention these purple hexagons. It does say " * By default, vscode will complete then to has_bind.and_then when you press enter. To disable this behavior, set "editor.acceptSuggestionOnEnter": false " though, which I think is not true: it should be the string "off" rather than the bool false

Mario Carneiro (Apr 01 2018 at 20:11):

coinductive is a lean command, but it only supports coinductive predicates. It is defined as a user command in init/meta/coinductive_predicates.lean

Last updated: Dec 20 2023 at 11:08 UTC