Zulip Chat Archive

Stream: general

Topic: Are these tokens?


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

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

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

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:46):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:47):

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

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:49):

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

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:50):

there is def but no definition

view this post on Zulip Kenny Lau (Apr 01 2018 at 19:51):

wait, coinductive?

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:51):

there is theorem though.

view this post on Zulip Kenny Lau (Apr 01 2018 at 19:51):

wait, I thought we don't have coinductive!

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:51):

VS Code says it's there

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:51):

but then again I thought we had definitions

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:51):

and VS Code says no

view this post on Zulip Kenny Lau (Apr 01 2018 at 19:52):

nah, coinductive hasn't been implemented

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:52):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:52):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:52):

I think you get an achievement for that error

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:53):

I'll give you an octopus

view this post on Zulip Kenny Lau (Apr 01 2018 at 19:53):

thanks

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:54):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:54):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:56):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:56):

which might mean "string"

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:58):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 19:59):

Maybe purple cube means "identifier"

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

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