Apply syntax question

Stream: new members

[Andre Popovitch]

Can I do

apply implication at binding,

as a shorthand for

have binding := implication(binding),

?

[Eric Wieser]

No, but I think that's been suggested before, and people were in favor of it

[Eric Wieser]

Maybe someone not on mobile can find the old thread

[Andrew Yang]

I think this is the one
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/modus.20ponens.20in.20context

[Mario Carneiro]

I think this is tactic#apply_fun?

[Ruben Van de Velde]

I was thinking apply_fun as well, but apparently that only works with equality and inequality. Should it be added?

[Eric Rodriguez]

I'm also still in favour of adding a coe_fun to iffs, which sort of links in

[Eric Wieser]

I don't really see the relation to apply imp at h, but this is a zulip thread regarding the has_coe_to_fun you mention.

[Eric Rodriguez]

well, it seems to me like the sort of "things you'd do in text maths that you can't yet do in Lean"