История изменений
Исправление AndreyKl, (текущая версия) :
Ну, не разрешима в общем случае. Иначе бы не существовало верных утверждений которые нельзя доказать. А они (в рамках зависимых типов) существуют. Соответсвенно солвер построить нельзя.
Правда с подсказками получается весьма интересно. В cpdt (книжка по коку) солвер всю рутину решает прям, если подсказки давать. Автор его назвал crush, что честно говоря отражает суть.. Попробую его к аргмаксу, когда время найду (вот сегодня можно было, но всё на ЛОР потратил :) )
Исправление AndreyKl, :
Ну, не разрешима в общем случае. Иначе бы не существовало верных утверждений которые нельзя доказать. А они (в рамках зависимых типов) существуют. Соответсвенно солвер построить нельзя.
Правда с подсказками получается весьма интересно. В cpdt (книжка по коку) солвер всю рутину решает прям, если подсказки давать. Автор его назвал crush, что честно говоря отражает суть..
Исправление AndreyKl, :
Ну, не разрешима в общем случае. Иначе бы не существовало верных утверждений которые нельзя доказать. А они (в рамках зависимых типов) существуют. Соответсвенно солвер построить нельзя.
Правда с подсказками получается весьма интересно. В cpdt солвер всю рутину решает прям, если подсказки давать.
Исходная версия AndreyKl, :
Ну, не разрешима в общем случае. Иначе бы не существовало утверждений которые нельзя доказать. А они (в рамках зависимых типов) существуют. Соответсвенно солвер построить нельзя.
Правда с подсказками получается весьма интересно. В cpdt солвер всю рутину решает прям, если подсказки давать.