Eta expand a function

Stream: Is there code for X?

[Arnav Sabharwal]

Is there a way to eta expand a metavariable for a function, whilst maintaining type (as in non-Expr based return type)? Thanks!

[Matt Diamond]

not sure if this is what you're looking for, but there's an eta_expand tactic