Если я правильно понимаю (в основном из-за наличия функции applyTactic), то можно написать собственную тактику для доказателя теорем в Идрисе. Какие (или где) примеры я мог бы использовать, чтобы узнать, как это сделать?
Пользовательская тактика прувера в Идрисе
comment
Я ничего не знаю о том, как его написать и использовать, но недавно я видел пример пользовательской тактики и пример использования. Надеюсь, это поможет.
- person laughedelic schedule 15.04.2014
comment
Приведенные выше ссылки больше недействительны, поскольку они относятся к HEAD репозитория. Вместо этого см. здесь: сначала, второй
- person max taldykin schedule 25.07.2014
Ответы (1)
В Idris есть два механизма написания пользовательских тактик: высокоуровневое и низкоуровневое отражение.
Используя высокоуровневую рефлексию, вы пишете функцию, которая работает с синтаксисом, а не с вычисляемыми данными — она не уменьшит свой аргумент. Эти функции возвращают новую тактику, определенную с использованием уже существующей тактики в Идрисе. Если вы хотите вернуть проверочный термин напрямую, вы всегда можете просто использовать Exact. Пример такого отражения можно найти в библиотека эффектов. Тактика отражения высокого уровня вызывается с помощью byReflection в режиме проверки.
При низкоуровневой рефлексии вы работаете напрямую с цитируемыми терминами из основной теории типов Идриса. Тогда тактика — это функция в TT -> List (TTName, TT) -> Tactic, где первый аргумент — тип цели, второй — контекст локального доказательства, а возвращаемый результат такой же, как и при высокоуровневом отражении. Это то, на что смехотворец ссылался выше. Они вызываются с помощью applyTactic в режиме проверки.
person
David Christiansen
schedule
17.04.2014
