問題タブ [coq-plugin]

関数を使用してメジャーを使用して再帰的定義を定義しようとしていますが、エラーが発生します：

ソースコード全体を一番下に投稿していますが、私の関数は

私は問題がforallsに起因することを知っています：それらをTrueに置き換えると、それは機能します。また、右側で含意（->）を使用すると、同じエラーが発生することもわかっています。Fixpointはforallsで機能しますが、メジャーを定義することはできません。

何かアドバイス？

約束通り、私の完全なコードは次のとおりです。

Coq 書き換えタクティクス モジュロ結合性と可換性をテストしていました ( aac_tactics)。次の例は整数 ( Z) に対して機能しますが、整数を有理数 ( ) に置き換えるとエラーが発生しますQ。

などで置き換えるRequire Import ZArith.とRequire Import QArith.、エラーが発生します。

エラー: 戦術の失敗: AC を法とする一致するオカレンスが見つかりません。

でaac_rewrite H.

との間に同様の不一致の問題がZあり、 /スコープが開いQているかどうかに関連していることが判明しました。ZQ

しかし、ここで aac の書き換えが機能しなかった理由がわかりません。Z不一致の原因は何ですか? また、とで同じように動作させるにはどうすればよいQですか?

tcoqをインストールしようとしたところ、次のエラーが発生しました。

誰かが知っていますか：

1. エラーの意味
2. 修正方法は？

関連する投稿をオンラインで見ました：

https://coq-club.inria.narkive.com/h4i0KOH0/problem-compiling-coq

しかし、それはあまり役に立ちませんでした。やった：

彼らが示唆したように、それはうまく機能しているようです...

私はそうしmake cleanましたが、それは役に立ちませんでした。

INSTALL のステップ 3 をスキップしたことに気付きましたが、それが問題に関連しているのか、それとも何をするつもりなのかはわかりません。

ゲームパッドをインストールしようとしていますが、そのためには指示に従う必要があります。具体的には、次の 3 つのコマンドを実行しました。

最新のエラー:

そのエラーを読んだ後、奇跡的に と の両方のバージョンを印刷することが思いつきましocamlたcamlp5:

と：

明らかにそれは間違っているので、おそらく最初のステップは、それが私が必要とするものであるためcamlp5、動作するように修正する4.05.0ことです.

アンインストールしようとしcamlp5ましたが、拒否されました。