問題タブ [coq-extraction]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
coq - タイプスキームの抽出
Coq で書いたファイル システム コードを抽出しようとしています。FileIOモナドを Haskell のモナドに置き換えたいIO。私のコードは次のようになります。
置換syncは問題ありませんが、置換しようとするとFileIO次IOのエラーが発生します。
このエラーは何を意味し、どうすれば回避できますか?
macos - Coq 抽出: 許可が拒否されました
CoqIDE 内で次のコマンドを実行すると:
次のエラーが表示されます。
代わりに試してみると：
エラーが発生します：
MacOSX 用の CoqIDE 8.5beta3 を使用しています。
どうすればこれを修正できますか? 権限の問題なしに CoqIDE を介して抽出を行うにはどうすればよいですか?
coq - Coq CompCert の EvalOp とは
EvalOp の定義は次のとおりですcompcert.backend.SplitLongproof。
この定義の奇妙な点は、andを 2 つの別個のトークンとしてcoqdoc --html認識していることです。EvalOp
Coq は、間に区切り文字 (スペース) のない 2 つのトークンを許可するのはなぜですか? それともこれはのバグcoqdocですか？助けてくれてありがとう！