Mathis Bouverot-Dupuis (May 11 2022 at 18:34): 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 ?
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
Mathis Bouverot-Dupuis (May 11 2022 at 19:53):pattern did the trick, thanks !
Notification Bot (May 12 2022 at 17:41):Mathis Bouverot-Dupuis has marked this topic as resolved.
Last updated: Oct 01 2023 at 19:01 UTC