printing `inferInstance`

Stream: mathlib4

[Thomas Browning]

I'm working on my first port, and ran into my first problem :D

This fails:

instance [Inhabited α] : Inhabited (Vector3 α n) :=
  Pi.inhabited _

because Lean doesn't recognize Pi.inhabited (it comes from the core of Lean3, so maybe it needs to be ported manually).

But in this case, this works:

instance my_instance [Inhabited α] : Inhabited (Fin2 n → α) :=
  inferInstance

But is there any way to figure out the name of the instance that inferInstance found?

[Scott Morrison]

#synth

[Mario Carneiro]

I am planning to make #synth [binders] : expr work, in which case you can easily check whether an instance exists by deleting instance foo and replace it with #synth

[Mario Carneiro]

But I think we can also have a linter for this