Question

Is there a way to do partial application for functions in Dafny?

Answer

Given

function f(i: int, j: int): int {...}

one can create a new partially-evaluated function, say evaluating the first argument at 2, by writing the lambda expression k => f(2,k). But note that this does not do any evaluation, partial or not. It merely defines a new function f' of one argument, such at f'(k) is f(2,k).

Dafny does not permit the syntax f(2) as a shorthand for k => f(2,k).