## Stream: general

### Topic: find data necessary for instances

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

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

#### Rob Lewis (Jan 09 2019 at 08:49):

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

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

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

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

#### Kevin Buzzard (Jan 09 2019 at 08:52):

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

#### Joey van Langen (Jan 09 2019 at 08:53):

Thanks! Is there also a generate skeleton for emacs?

#### Reid Barton (Jan 09 2019 at 08:54):

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

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

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

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