Zulip Chat Archive

Stream: new members

Topic: Explicitly specifying one particular argument


view this post on Zulip 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

view this post on Zulip Julian Berman (Oct 11 2020 at 00:11):

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

view this post on Zulip 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.

view this post on Zulip 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₂.

view this post on Zulip Pedro Minicz (Oct 11 2020 at 01:41):

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

view this post on Zulip 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"

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Oct 11 2020 at 08:36):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Eric Wieser (Oct 11 2020 at 09:09):

You could replace explicit with a suitable unicode character?

view this post on Zulip Mario Carneiro (Oct 11 2020 at 09:16):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Oct 11 2020 at 14:16):

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

view this post on Zulip 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

view this post on Zulip 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