4 
PA6 : ∀{m n} -> m ≡ n -> n ≡ m

は、私が解決してサポートしようとしている公理です。(コア ライブラリの) cong を使用してみましたが、cong コンストラクターに問題があります。

PA6 = cong

cong の場合、等値と型の refl を指定する必要があることはわかっていますが、どの型を指定すればよいかわかりません。アイデア？

これは大学での小さな課題のためなので、実際の回答を書くよりも、私が見逃していたことを誰かに示してもらいたいのですが、ある程度のサポートをお願いします.

4

2 に答える 2

7

あなたのPA6は、≡が対称であると言います。

これは、Relation.Binary.PropositionalEquality モジュールの標準ライブラリにあります。

sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

(この質問はかなり古いものですが、偶然見つけた将来の読者のために投稿しています。)

于 2010-11-07T19:48:35.483 に答える
3

私が作成したシステムの性質上、2 つの同値があることを認識しなければならなかったため、同値メソッド refl を使用する必要がありました。

したがって、私の型シグネチャを満たすために agda は受け入れました:PA6 refl = refl

それが役立つことを願っています

于 2010-04-05T07:03:33.317 に答える