proof-general

1熱

2答えて

私はemacsでCoqを勉強しています。私はemacsウィンドウを縦に吐き出し、左はドキュメントで、右はコード編集エリアです。 Coqプログラムを解釈すると、結果は左側のウィンドウに表示され、文書をカバーします。これは私を悩ます。コード編集領域を水平に分割して解釈結果が右下に表示されるような方法はありますか？

9熱

1答えて

EmacsのCoq/Proofのキーワードと演算子のUnicodeグリフ

この質問は、EmacsのProof General内でCoqモードを設定することと関係しています。私はEmacsが自動的にCoqのキーワードと表記を対応するUnicodeグリフに置き換えようとしています。私はfunをギリシャの小文字のラムダλ、forallと定義して、ユニバーサル限定記号∀などとしました。私は単語の記号を定義することに問題はありませんでした。問題は、私は彼らのUnicodeのシ

7熱

2答えて

Coq/Proof GeneralのAgdaのようなプログラミングですか？

Agdaとは異なり、Coqは証明と機能を分離する傾向があります。 Coqが提供する戦術は、校正を書くのに最適ですが、Agdaモードの機能を再現する方法があるかどうかは疑問です。具体的には、私がしたい： Agdaの?やHaskellの_の一部と同等に、私はそれを書いている間、機能の一部を省略し、（たぶん）コックは私伝える持つことができる場所タイプ私はあなたが機能して?ブロックを埋めるAgdaモード

4熱

3答えて

emacsでVerilogモードを無効にする方法は？

私はProofGeneralでcoqを使用しようとしていますが、組み込みVerilogモードではファイルタイプ認識*.vが影になっています。私はどうにかそれを無効にして、ProofGeneralをcoqモードに再マップさせることはできますか？

5熱

2答えて

Isabelle2016 and Proof General

私はIsabelle 2016を使用することを学びました。原理的には私は非同期証明チェックの考え方が好きですが、Isabelle/jEditはいくつかの理由で好きではありません。あまりにも多くのメモリを使用しているということです（私にとって）。私はIsabelle 2016で良い古いProof Generalを使用することができれば嬉しいです。isa-isabelle-commandという変数を