Stream: Coq users

Topic: ✔ rewriting to isolate term


view this post on Zulip Mathis Bouverot-Dupuis (May 11 2022 at 18:34):

Hi everyone, I have a goal of the form <some expression containing t> with t a term, and I would like to rewrite it to (fun t0 => <some expression involving t0>) t. Is there a tactic to do this ?

view this post on Zulip Paolo Giarrusso (May 11 2022 at 19:29):

Something like set (x := t). pattern t. should do it but I forget the exact syntax for set

view this post on Zulip Mathis Bouverot-Dupuis (May 11 2022 at 19:53):

pattern did the trick, thanks !

view this post on Zulip Notification Bot (May 12 2022 at 17:41):

Mathis Bouverot-Dupuis has marked this topic as resolved.


Last updated: Jun 15 2024 at 08:01 UTC