Zulip Chat Archive

Stream: new members

Topic: Apply syntax question


Andre Popovitch (Dec 08 2021 at 23:51):

Can I do

apply implication at binding,

as a shorthand for

have binding := implication(binding),

?

Eric Wieser (Dec 08 2021 at 23:55):

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

Eric Wieser (Dec 08 2021 at 23:55):

Maybe someone not on mobile can find the old thread

Andrew Yang (Dec 08 2021 at 23:57):

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 (Dec 09 2021 at 03:40):

I think this is tactic#apply_fun?

Ruben Van de Velde (Dec 09 2021 at 14:40):

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

Eric Rodriguez (Dec 09 2021 at 15:01):

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

Eric Wieser (Dec 09 2021 at 15:54):

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 (Dec 09 2021 at 16:12):

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


Last updated: Dec 20 2023 at 11:08 UTC