Idris의 맞춤형 증명자 전술

Question

내가 올바르게 이해했다면 (주로 applyTactic 함수), Idris에서 정리 증명자에 대한 사용자 정의 전술을 작성하는 것이 가능합니다.이를 수행하는 방법을 배우기 위해 사용할 수 있는 몇 가지 예는 무엇입니까?

Answer 1

Idris에는 사용자 지정 전술을 작성하는 두 가지 메커니즘이 있습니다.높은 수준과 낮은 수준의 반사.

높은 수준의 리플렉션을 사용하여 평가된 데이터가 아닌 구문에 따라 실행되는 함수를 작성합니다. 인수가 줄어들지는 않습니다.이 함수는 Idris의 기존 전술을 사용하여 정의된 새로운 전술을 반환합니다.증명 용어를 직접 반환하려면 언제든지 다음을 사용할 수 있습니다. Exact.이런 종류의 반성의 예는 다음에서 찾을 수 있습니다. 효과 라이브러리.다음을 사용하여 높은 수준의 반사 전술이 호출됩니다. byReflection 증명 모드에서.

낮은 수준의 반영에서는 Idris의 핵심 유형 이론에서 인용된 용어를 직접 사용하여 작업합니다.그러면 전술은 다음의 기능이 됩니다. TT -> List (TTName, TT) -> Tactic 여기서 첫 번째 인수는 목표 유형이고 두 번째 인수는 로컬 증명 컨텍스트이며 반환 결과는 상위 수준 리플렉션과 동일합니다.이것이 Laughadelic에 연결된 것입니다. ~ 위에.이는 다음을 사용하여 호출됩니다. applyTactic 증명 모드에서.