Stream: Coq users

Topic: Name mangling and `(e)apply ... with`


view this post on Zulip Ralf Jung (Oct 22 2020 at 11:28):

Is there any way at all to use (e)apply ... with (name:=val) when name mangling is enabled? It seems like that should be possible, given in particular that term (name:=val) does work with name mangling. But so far I failed to get this to work. This fails:

Set Mangle Names.

Lemma lem1 (P Q: Prop) : P -> Q -> P.
Proof. auto. Qed.

Goal True. Proof.
eapply lem1 with (Q:=True).

view this post on Zulip Ralf Jung (Oct 22 2020 at 11:28):

And speaking of with, it'd be great if someone could explain this behavior ;) (EDIT: @Pierre-Marie P├ędrot already did)

view this post on Zulip Ralf Jung (Oct 22 2020 at 11:29):

The inability to use with is particularly annoying since term (name:=val) unfortunately only works for implicit arguments

view this post on Zulip Ralf Jung (Oct 22 2020 at 11:33):

potentially related: https://github.com/coq/coq/issues/4536

view this post on Zulip Ralf Jung (Oct 22 2020 at 11:50):

for term (name:=val), a change was made to avoid refreshing names unnecessarily; I wonder if something similar could be done here?


Last updated: Jan 27 2023 at 01:03 UTC