Using `set f_ := @f`

makes path appear in the goal, like `Nat.f`

to distinguish between the alias and the original function.

From what I have tried the issue with Arguments, it that it is not local to a proof, so you have to reset Arguments after the proof

Ok, here is a solution using notations:

```
From Coq Require Import Utf8.
Definition f {A : Type} (x : A) := x.
Notation "'f{' A } x" := (@f A x) (format "f{ A } x", at level 20) : f_scope.
Goal ∀ A x, @f A x = x.
Proof.
intros A x. (* f x = x *)
Open Scope f_scope. (* f{ A } x = x *)
Close Scope f_scope. (* f x = x *)
```

But I agree that it's not ideal. What I would like personally is to be able to interact with the goal in the editor to reveal implicits and such just by clicking or whatever.

That is not perfect but it is a cool solution

Thanks

Thomas Lamiaux has marked this topic as resolved.

Last updated: Jun 22 2024 at 16:02 UTC