compcert

0熱

1答えて

エラー：のCoQ

での評価の基準に強制することはできません私はMem.loadを展開しようとしていると私はエラーを取得する： Error: Cannot coerce Mem.load to an evaluable reference. 私はload1としてMem.loadのまったく同じDefinitionを書き、展開可能です。これは、それがunfold EDになることができないことを意味 Global Opaq

coq compcert 2016-10-14

---

0熱

1答えて

Coqで2つの 'int'型を比較す​​る方法はありますか？

私はCoqのスペックファイルに次の定義を持っています。私は2つの "int"型の値を比較する命題を持つ必要があります。これら2つは 't'と 'Int.repr（i。（period1））'です（i.period1）と（i.period2）はタイプ 'Z'です。 これは私のコードスニペットです：これは私に以下のエラーが発生します Definition trans_uni_r_reject (i: i

logic coq compcert 2016-07-26

---