Stream: Coq users

Topic: ✔ Displaying implicit arguments in a goal during a proof


view this post on Zulip Thomas Lamiaux (Apr 30 2024 at 06:55):

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

view this post on Zulip Théo Winterhalter (Apr 30 2024 at 07:26):

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.

view this post on Zulip Thomas Lamiaux (Apr 30 2024 at 07:34):

That is not perfect but it is a cool solution

view this post on Zulip Thomas Lamiaux (Apr 30 2024 at 07:34):

Thanks

view this post on Zulip Notification Bot (Apr 30 2024 at 07:56):

Thomas Lamiaux has marked this topic as resolved.


Last updated: Jun 22 2024 at 16:02 UTC