могут ли функции dafny возвращать две вещи так же, как и методы?

Although methods can return a pair consisting of two things (e.g. nats). Using a function I can only find how to return a single thing even if that is a pair (of nats).  This prevents me from using a single function to define a lexical decreases pair.

function twof() : (nat,nat) { (1,2)}
method twom() returns (r:  nat, r2: nat) { r,r2  := 5,6;} 

method Main() {
    var (x,y) := twof();
    //var x1,y1 := twof(); // Error
    var mx, my := twom();
}

Это разница между дафными функциями и методами или я что-то пропустил?