Индивидуальная тактика проверки в Идрисе

Question

Если я правильно это понимаю (главным образом, исходя из существования applyTactic функция), в Idris можно написать собственную тактику для доказательства теоремы.Какие (или где) есть примеры, которые я мог бы использовать, чтобы научиться это делать?

Answer 1

В Idris существует два механизма для написания пользовательских тактик:высокоуровневое и низкоуровневое отражение.

Используя высокоуровневое отражение, вы пишете функцию, которая работает с синтаксисом, а не с оцениваемыми данными - это не уменьшает ее аргумент.Эти функции возвращают новую тактику, определенную с использованием ранее существовавшей тактики в Idris.Если вы хотите вернуть термин доказательства напрямую, вы всегда можете просто использовать Exact.Пример такого рода размышлений можно найти в библиотека эффектов.Высокоуровневая тактика отражения вызывается с использованием byReflection в режиме проверки.

В низкоуровневом отражении вы работаете непосредственно с цитируемыми терминами из основной теории типов Идриса.Таким образом, тактика - это функция в TT -> List (TTName, TT) -> Tactic где первый аргумент - это тип цели, второй - локальный контекст доказательства, и возвращаемый результат такой же, как в высокоуровневом отражении.Это то, с чем связан laughadelic выше.Они вызываются с помощью applyTactic в режиме проверки.