0

自然界のセットを合計しようとしている自分に気づきました。単純なモデルを実行すると、次の動作に戸惑いました。

(次のコードが util/natural のコピーにあると仮定すると、 ord がインポートされます)

//sums the values in a set of naturals
fun setsum[nums : set Natural] : lone Natural {
    {n : Natural | #ord/prevs[n] = (sum x : nums | #ord/prevs[x])}
}

次に、util/natural のコピーをインポートするモジュールで:

private open mynatural as nat

let two = nat/add[nat/One, nat/One]
let three = nat/add[two, nat/One]
let four = nat/add[two, two]
let five  = nat/add[four,nat/One]

pred showExpectSum10 {
    some x : Natural | x in setsum[{n : Natural | nat/lt[n, five]}]
}

//run showExpectSum10 for 15 //result is 10, as expected
//run showExpectSum10 for 1 but 20 Natural //result is 10  as expected
run showExpectSum10 for 1 but 40 Natural //result is 26 somehow.

Natural のスコープを変更すると、結果がこのように影響を受けるのはなぜですか?

4

1 に答える 1