## Stream: new members

### Topic: Explicitly specifying one particular argument

#### Julian Berman (Oct 11 2020 at 00:08):

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 (Oct 11 2020 at 00:11):

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

#### Julian Berman (Oct 11 2020 at 00:13):

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 (Oct 11 2020 at 01:41):

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 (Oct 11 2020 at 01:41):

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

#### Julian Berman (Oct 11 2020 at 02:18):

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

#### Kevin Buzzard (Oct 11 2020 at 07:27):

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 (Oct 11 2020 at 08:36):

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

#### Mario Carneiro (Oct 11 2020 at 09:04):

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

#### Mario Carneiro (Oct 11 2020 at 09:06):

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 (Oct 11 2020 at 09:09):

You could replace explicit with a suitable unicode character?

#### Mario Carneiro (Oct 11 2020 at 09:16):

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

#### Julian Berman (Oct 11 2020 at 13:15):

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 (Oct 11 2020 at 13:18):

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 (Oct 11 2020 at 14:02):

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

#### Mario Carneiro (Oct 11 2020 at 14:16):

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

#### Mario Carneiro (Oct 11 2020 at 14:16):

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

#### Julian Berman (Oct 11 2020 at 14:22):

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

Last updated: May 14 2021 at 00:42 UTC