Итак, я пытаюсь получить все элементы из набора наборов, но получаю сообщение об ошибке:
«понимание множества должно производить конечное множество, но эвристика Дафни не может понять, как создать ограниченный набор значений для 'x'»
Я думаю, что это может быть связано с тем, что вы не можете получить кардинальность множества.
Ценю всю помощь.
function flatten(nested: set<set<int>>) : set<int>
{ set x | forall y :: y in nested && x in y :: x }
Возможно, следующее сделает то, что вы хотите:
function flatten(nested: set<set<int>>) : set<int>
{
set x, y | y in nested && x in y :: x
}
Ваше определение совсем другое. В нем говорится что-то вроде «набора элементов, такого, что для всех y всех типов set<int> y находится в nested, а x находится в y». Обычно это неверно (и поэтому бесполезно), поскольку требует, чтобы nested было конечным множеством, содержащим все множества типа set<int>.
Наконец, также обратите внимание, что вы можете получить количество элементов множества S, используя выражение |S|.
