Блог

В расширении Sledgehammer с помощью решателей SMT есть это утверждение:

Лямбда-абстракции переписываются в комбинаторы Тернера или преобразуются в явные функции с использованием лямбда-абстракций.

Связанная ссылка, переводящая предложения более высокого порядка в предложения первого порядка, не объясняет, как синхронизируется этот метод. Всегда ли мы используем их оба? Предпочтительнее ли одно другому?

Согласно mediatum.ub.tum.de/doc/1097834/1097834.pdf выбор метода адаптирован для каждого проверяющего.