Zulip Chat Archive
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):
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: Dec 20 2023 at 11:08 UTC