自然界のセットを合計しようとしている自分に気づきました。単純なモデルを実行すると、次の動作に戸惑いました。
(次のコードが 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 のスコープを変更すると、結果がこのように影響を受けるのはなぜですか?