Dafny编写斐波那契函数遇类型不匹配错误：预期nat却得到set

你的代码报错原因很明确：分支语句里的{}被Dafny解析成了集合字面量，而非代码块。

当你写{n}时，Dafny会认为你返回的是包含元素n的集合（类型为set<nat>），但函数声明的返回类型是nat，这就导致了「期望nat，得到set」的类型不匹配错误。

Dafny的函数体是单一表达式结构，分支返回值不需要用大括号包裹，直接写表达式即可。修正后的代码如下：

function fibo(n: nat) : nat 
{
   if n == 0 || n == 1 then
      n
   else
      fibo(n-1) + fibo(n-2)
}

补充说明：只有在需要执行多语句逻辑的method中，才会用大括号表示代码块；而function作为纯表达式计算的载体，直接返回表达式结果即可。

内容的提问来源于stack exchange，提问作者Sumit