Idris のカスタム証明者戦術

Question

私がそれを正しく理解していれば（主に applyTactic 関数) を使用すると、Idris の定理証明者用のカスタム戦術を記述することができます。その方法を学ぶために使用できる例は何 (またはどこ) ですか?

Answer 1

Idris でカスタム戦術を記述するためのメカニズムは 2 つあります。高レベル反射と低レベル反射。

高レベルのリフレクションを使用すると、評価されたデータではなく構文で実行される関数を作成できます。引数は減りません。これらの関数は、Idris の既存の戦術を使用して定義された新しい戦術を返します。証明項を直接返したい場合は、いつでも使用できます Exact. 。この種の反映の例は次のとおりです。 エフェクトライブラリ. 。高レベルのリフレクション戦術は、以下を使用して呼び出されます。 byReflection プルーフモードで。

低レベルのリフレクションでは、イドリスの中核となる型理論から引用された用語を直接操作します。したがって、戦術は次の機能になります。 TT -> List (TTName, TT) -> Tactic ここで、最初の引数はゴールの型、2 番目の引数はローカル証明コンテキストで、返される結果は高レベルのリフレクションの場合と同じです。これは、Laughadelic がリンクしたものです その上. 。これらは次を使用して呼び出されます applyTactic プルーフモードで。