## 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

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: May 15 2021 at 02:11 UTC