私はこれを何時間も理解できずに見つめていました:(
coq を使用していくつかの定義を解決する必要があり、Curry Howard 同型を介して解決することになっています。私は読んだことがありますが、自分が何をしているのかまだわかりません。私は他の例を見て、そのようにしてみましたが、常にエラーが発生します。
たとえば、ここでは次のように定義する必要があります。
Variables A B C : Set.
Definition c01 : (A -> B -> C) -> (B -> A -> C) :=
これは私の試みでした：
fun g => fun p => g (snd p) (fst p).
end.
私も試しました
fun f => fun b => fun a => f (b , a)
end.
最終的には、私が与えたものとは異なるタイプを期待していたとだけで、「タイプが「?9 * ?10」であると予想される」などのように表示されることもあります。
私が見つけたすべてを読んだ後、これを理解するのに本当に苦労しています。
誰か説明してください:(