## Stream: general

### Topic: don't try tc inference on _ arguments

#### Johan Commelin (Oct 27 2020 at 18:42):

Sometimes Lean isn't being smart when you tell it refine my_lemma x, and so you say refine @my_lemma _ _ _ _ x. But then the 2nd _ is some typeclass argument that Lean can't find, and so the refine fails. Instead, I would like it to turn that argument into a new goal.
Of course _ is powerful the way it is, so we shouldn't change that.

Can we make … mean roughly the same to Lean, except that it will just blindly turn that argument into a goal, without trying to infer it by elaboration or typeclass search?

#### Reid Barton (Oct 27 2020 at 18:43):

:four_leaf_clover:

#### Gabriel Ebner (Oct 27 2020 at 18:43):

Does notation … := id _ work?

#### Gabriel Ebner (Oct 27 2020 at 18:43):

That's @Mario Carneiro's standard trick.

#### Johan Commelin (Oct 27 2020 at 18:44):

I haven't tried yet.

#### Reid Barton (Oct 27 2020 at 18:44):

I wish it was easier to experiment with Lean 4, since I think this exact feature already exists.

#### Reid Barton (Oct 27 2020 at 18:44):

Well, not using the name …

#### Gabriel Ebner (Oct 27 2020 at 18:45):

I think it's refine @my_lemma ?inst_1 ?inst_2 etc.

#### Gabriel Ebner (Oct 27 2020 at 18:45):

Errm, I mean refine @myLemma ?inst1 ?inst2 of course.

#### Reid Barton (Oct 27 2020 at 18:45):

Yes, something with question marks

#### Gabriel Ebner (Oct 27 2020 at 18:46):

https://github.com/leanprover/lean4/blob/8e16589f603f3425119df8533fda9204ff6b0599/tests/lean/namedHoles.lean

#### Reid Barton (Oct 27 2020 at 18:47):

I think maybe also a ? without a name is a fresh hole. I didn't realize there were named holes, that seems neat though I'm not sure offhand where it would come up...

#### Gabriel Ebner (Oct 27 2020 at 18:49):

Unnamed holes are ?_ IIRC.

Last updated: May 12 2021 at 04:19 UTC