为什么会出现此打字问题？

Question

我正在尝试用 Dafny 编写程序，这是程序的一部分：

method GenerateAllIndexSubsets<T>(q: seq<T>) returns (res: set<set<nat>>)
    ensures res == AllIndexSubsets(q)
{
    if |q| == 0
        { 
        assert |q| == 0;// if's guard
        // ==>
        assert {} == AllIndexSubsets<nat>([]);
        assert q == [];
        assert {} == AllIndexSubsets(q);
        res := {};
        assert res == AllIndexSubsets(q); // postcondition
        }
    else
        { 
            assert |q| != 0; // !(if's guard)
            var res0 : set<set<nat>> := GenerateAllIndexSubsets<T>(q[1..]);
            assert res0 == AllIndexSubsets(q[1..]);
            res := res0;    
            assert res ==  AllIndexSubsets(q[1..]); //GenerateAllIndexSubsets postcondition with q[1..]
            var index : nat := q[0];
            var res1: set<set<nat>> := (set x | x in res0 :: x + {index});
            assert res1 == AllIndexSubsets(q) - AllIndexSubsets(q[1..]);
            assert res0 == AllIndexSubsets(q[1..]);
            assert res1 == AllIndexSubsets(q) - res0;
            // ==>
            assert res0 + res1 == AllIndexSubsets(q);
            res := res + res1;
            assert res == AllIndexSubsets(q); // postcondition
        }
    assert res == AllIndexSubsets(q); // postcondition
}

在线 var index : nat := q[0] 我遇到以下问题：

type does not agree with element type seq (got int)

为什么我会得到这个问题，我现在如何解决它并且以后不会再得到它？

Answer 1

q 是 T 类型元素的序列，因此 q[0] 具有 T 类型。但是您试图将其分配给 nat 类型的变量，这是不正确的。

（Dafny 错误消息提到 int 而不是 nat 的原因是 nat 被定义为 int 的子集，所以为了检查某物是否为 nat，Dafny 首先检查它是否为 int，此处失败。）

为什么会出现此打字问题？

Why does this typing issue occur?

types

dafny