types - 为什么会出现这个打字问题？

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]我遇到以下问题：

类型与元素类型 seq 不一致（得到 int）

为什么我会得到这个，我怎么能现在解决它而不是将来再次得到它？

Answer 1

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

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