Explicitly specifying one particular argument

Stream: new members

[Julian Berman]

Hi. Is there a "less drastic" version of @foo if I want to only explicitly provide one particular implicit parameter rather than all of them? I have a thing with implicit arguments that somehow lean is having trouble unifying automatically, which works if I use @foo, but I suspect it's one particular argument that lean's having trouble with, whereas now I have to specify like 8 things

[Julian Berman]

Ah OK I guess I can go sprinkle back in _'s to the @foo call.

[Julian Berman]

Yeah that works, never mind :) I guess it's 2 of my 9 arguments lean is not figuring out on its own... interesting.

[Pedro Minicz]

Although not directly related, but you can specify arguments to be "partially hidden" (I am sure there is an official name for this, which I am not aware of), like in function.injective:

@[reducible] def injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂

Given hf : function.injective f you can apply h a₁ a₂ or hf h where a₁ a₂ : α and h : f a₁ = f a₂.

[Pedro Minicz]

I think this is a pretty cool feature that should be used more (including in mathlib!).

[Julian Berman]

Ah interesting thanks. I saw those mentioned in the ref manual, it calls them "implicit arguments weakly inserted"

[Kevin Buzzard]

But we lack the full flexibility to be able to do this -- supplying just one or two implicit variables and letting lean do the rest. Maybe lean 4?

[Eric Wieser]

Could a tactic be created to do this? Something like by explicit foo x=1?

[Mario Carneiro]

It seems like you would have to have quite a few arguments before that pays off in terms of characters

[Mario Carneiro]

Plus the most common reason you want this is to supply an instance argument and those are typically anonymous, so they don't have names to refer to anyway (unless you like _inst_4)

[Eric Wieser]

You could replace explicit with a suitable unicode character?

[Mario Carneiro]

plus parsing the syntax you gave there is going to be hard for a tactic

[Julian Berman]

Eric Wieser said:

You could replace explicit with a suitable unicode character?

Or = with one, no? Having some sort of named argument syntax seems like it'd solve things but I guess that's trickier in lean where x=3 is way better served as being that equality rather than argument syntax

[Julian Berman]

Oh wait or I guess the suggestion of having it be a tactic is that that way nothing low level needs to be added/changed

[Eric Wieser]

Exactly; I'm not saying "it should be spelt like this", but "you could build a spelling like this without changing lean"

[Mario Carneiro]

The hard part about parsing the syntax is that it's all expressions without any separators

[Mario Carneiro]

did you ever notice that tactics always have a healthy portion of filler words like using, with etc

[Julian Berman]

Yes -- is that also why record notation has that . between the structure name and its arguments