find data necessary for instances

Stream: general

[Joey van Langen]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Joey van Langen]

Thanks! Is there also a generate skeleton for emacs?

[Reid Barton]

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

[Joey van Langen]

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

[Reid Barton]

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

[Reid Barton]

It requires importing the mathlib module that Rob mentioned