unfold partial application

Stream: general

[Pablo Le Hénaff]

Hey.
I'm trying to unfold my own definition which is only applied partially, e.g.
in a goal

finset.sum (S : finset α) (my_function b) = something_else

where

my_function : some_type -> α -> some_comm_monoid_type

In that case, dunfold/unfold doesn't work and I need to specify

finset.sum (S : finset α) (λa, my_function b a) = something_else

for the tactic to work. Is there a workaround for this to be done automatically ? Thanks.

[Mario Carneiro]

You can define my_function with the second argument right of the colon

[Mario Carneiro]

i.e. write my_function (s : some_type) : α -> some_comm_monoid_type := λa, ...

[Mario Carneiro]

assuming you always want to unfold this function in such a partially applied environment