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).
And speaking of
with, it'd be great if someone could explain this behavior ;) (EDIT: @Pierre-Marie Pédrot already did)
The inability to use
with is particularly annoying since
term (name:=val) unfortunately only works for implicit arguments
potentially related: https://github.com/coq/coq/issues/4536
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