在 dafny 中评估后缀语言的递归算法

如何解决在 dafny 中评估后缀语言的递归算法

我有这个数据类型的序列

datatype Op = Operand(int) | Addition | Multiplication

我编写了以下评估函数，但它不起作用。 （我认为递归不正确，但我不知道如何解决。）

function method ValueOfPostFix(postfix: seq<Op>,index : nat): int
requires 0 <= index < |postfix|
decreases index
{
    match postfix[index]
    {
        case  Operand(x) => x   
        case Multiplication => if (index > 0) then ValueOfPostFix(postfix,index-1) * 
                                   ValueOfPostFix(postfix,index-1)
                                   else 0   
        case Addition => if (index > 0) then ValueOfPostFix(postfix,index-1) + 
                             ValueOfPostFix(postfix,index-1)
                             else 0
    }
}