structure stubs

Stream: general

[Simon Hudon]

I just created a hole command for filling in the fields of a structure when trying to write an instance. Does this look useful to the community and is there a different way it should work?

https://github.com/leanprover/mathlib/pull/397

[Reid Barton]

Not able to try this right now but this is something I've wanted often