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 ?

Something like `set (x := t). pattern t.`

should do it but I forget the exact syntax for set

`pattern`

did the trick, thanks !

Mathis Bouverot-Dupuis has marked this topic as resolved.

Last updated: Jun 15 2024 at 08:01 UTC