Я пытаюсь скомпилировать свой код Леона, используя scalac напрямую. К сожалению, мне не удалось правильно собрать библиотеку Leon, от которой зависит код. Например, я запустил scalac $(find ~/my-path/leon/library/ -name "*.scala" | xargs)...

При работе с Welder я столкнулся с ситуацией, когда мне нужно доказать, что: если content(l1) == content(l2) и f является идемпотентным, ассоциативным и коммутативным оператором, то fold(f,z,l1) = fold(f,z,l2) На одном этапе доказательства...