proof-general

4зной

2ответ

Как вы смотрите, где идентификаторы определены в Coq эффективно?

В большинстве IDE или текстовых редакторах вы можете щелкнуть правой кнопкой мыши по термину и передать его в файл, где этот термин определен. CoqIDE, похоже, не имеет этого, поэтому я делал coqdoc my

9зной

1ответ

Глифы Юникода для ключевых слов и операторов в Coq/Proof General под Emacs

Этот вопрос связан с настройкой режима Coq в разделе Proof General в Emacs. Я пытаюсь, чтобы Emacs автоматически заменил ключевые слова и обозначения в Coq соответствующими символами Unicode. Мне удал

7зной

2ответ

Агдаподобное программирование в Coq/Proof General?

В отличие от Agda, Coq имеет тенденцию отделять доказательства от функций. Тактика Coq дает отличные возможности для написания доказательств, но мне интересно, есть ли способ воспроизвести некоторые ф

4зной

1ответ

Как отображать скобки вокруг предположений в Isabelle/jEdit?

Когда цели отображаются Isabelle в ProofGeneral, предположения оказываются как имеющие скобки вокруг них, как так: В Isabelle/jEdit, однако, это, похоже, изменилась к мета-импликации стрелки: в то вре