Stream: Coq users

Topic: How to generate fresh hypothesis names


view this post on Zulip Ricardo Almeida (Jun 20 2023 at 17:34):

Hi, I find that this section of the manual on how to generate fresh hypothesis names is incomplete. It says that fresh component* evaluates to an identifier unbound in the goal, which is what I need, but how do I use it? Should it be, for instance, intro (fresh "G")? Or intros x; fresh "G" as G, or something else? All I've tried fails.
Thanks in advance.

view this post on Zulip Kenji Maillard (Jun 20 2023 at 17:42):

You should let-bind the result of fresh: let x := fresh "G" in intros x.

view this post on Zulip Ricardo Almeida (Jun 20 2023 at 17:51):

Awesome, thanks!


Last updated: Jun 23 2024 at 03:02 UTC