Zulip Chat Archive

Stream: general

Topic: find data necessary for instances


view this post on Zulip Joey van Langen (Jan 09 2019 at 08:47):

Is there an easy way to find which fields should be provided when defining an instance?
For example making an instance of a ring requires you to fill in a lot of data from different classes and manually going through each class in the hierarchy and finding the names of the respective data is quite some work

view this post on Zulip Rob Lewis (Jan 09 2019 at 08:49):

One method is a hole command, as seen briefly in Mario's coding session yesterday:

variable α : Type
example : ring α :=
{! !}

In VSCode, click on the lightbulb and choose "generate a skeleton for the structure."

view this post on Zulip Rob Lewis (Jan 09 2019 at 08:49):

(You'll need the right import, probably mathlib's tactic.interactive, I don't remember.)

view this post on Zulip Kevin Buzzard (Jan 09 2019 at 08:50):

If I type

example (R : Type) : ring R :=
{

}

then (in VS Code) in the "problems" window (which I sometimes need to create by "pulling up" near the bottom of VS Code) then I see 15 problems, one for each field I need to create. Does this help?

view this post on Zulip Rob Lewis (Jan 09 2019 at 08:50):

Alternatively, you can just write an empty structure {} and look at the error messages. (What Kevin said.)

view this post on Zulip Kevin Buzzard (Jan 09 2019 at 08:50):

Within the { } Lean is expecting me to write add := blah etc, and I get a problem for each missing field.

view this post on Zulip Kevin Buzzard (Jan 09 2019 at 08:52):

Rob's import is correct -- I just tried it.

view this post on Zulip Joey van Langen (Jan 09 2019 at 08:53):

Thanks! Is there also a generate skeleton for emacs?

view this post on Zulip Reid Barton (Jan 09 2019 at 08:54):

Yes, move the cursor inside the {! !} and press C-c SPC

view this post on Zulip Joey van Langen (Jan 09 2019 at 08:58):

Not having much succes with the C-c SPC. What should I enter when asked for a hole command?

view this post on Zulip Reid Barton (Jan 09 2019 at 09:00):

If you press tab, one of the options should be "Instance Stub — Generate a skeleton for the structure under construction."

view this post on Zulip Reid Barton (Jan 09 2019 at 09:00):

It requires importing the mathlib module that Rob mentioned


Last updated: May 16 2021 at 05:21 UTC