Я пытаюсь доказать поставленный выше вопрос. Мне дали определение индукции: Definition nat_ind (p : nat -> Prop) (basis : p 0) (step : forall n, p n -> p (S n)) : forall n, p n := fix f n := match n return p n with |...

Импликационная связка печатается как лямбда-выражение в моем coqide (OS X El Capitan). это ожидаемое поведение? Я бы предпочел видеть их напечатанными, как в coqtop . Мне не удалось найти параметр / параметр командной строки для изменения стиля...

Я читаю логические основы и скачал поставляемые скрипты coq с этим. Пользуюсь coq v8.8.1, установка через opam. Я получаю две ошибки в заголовке, и я не уверен, как мне их отлаживать. Полное сообщение об ошибке для второй ошибки: COQDEP...

Я хочу получить результат компиляции файла. v от coqide или coqc для лечения с помощью java, скорее у меня есть лечение автомата, и я хочу построить графический интерфейс этого автомата на java. Спасибо за ваш ответ.

В документе Coq XML Protocol (для Добавить операцию) , строка имеет вид <int>${editId}</int> . Что такое editID здесь? Я спросил об этом, потому что мне не удалось взаимодействовать с coqtop в режиме ideslave. Используя...

По какой-то причине мой файл Coq не компилируется. Я использую CoqIDE в Windows 10. Когда я использую инструмент Compile->Compile buffer , я получаю С другой стороны, когда я использую инструмент Compile->Make , я получаю...

Я использую протокол XML из Coq 8.6.1. Когда я попробовал вызов PrintAst, мне не удалось получить AST, но вместо этого я получил «todo». Это неисправность или я что-то не так сделал? Как мне получить AST из вызова print AST? Вот мой случай: я...

У меня уже установлен Coq, теперь я пытаюсь установить CoqIDE на Mac. Я слежу за вики Coq . Сборка завершается ошибкой на втором этапе. Когда я бегу ш gtk-osx-сборка-setup.sh Это ошибка, которую я получаю: Checking out jhbuild...

моя проблема кажется распространенной, но ни один из найденных ответов не смог ее решить. Я слежу за курсом по основам программного обеспечения на Coq, поэтому подхожу к команде: > From LF Require Export Basics. Что бы я ни пытался, я...

У меня есть две равные подцели: prove_me (x::xs) = true prove_me (x::xs) = true Доказательства будут равны. Как я могу решить вторую цель, используя первую?

Я новичок в Коке. У меня есть тип записи и одно определение: Record t : Type := T { width : nat; }. Definition indent shift f := match f with | T w => T (w + shift) end. Я хочу доказать тривиальную лемму: Lemma...

Итак, я пытаюсь изучить Coq, используя сценарий «Введение в вычислительную логику», и мне дали упражнение. Это доказать следующее: «для всех a b, a + S b = S (a + b)». Мне дано определение "nat_ind": (p : nat -> Prop) (basis : p 0)...

Я следую главе «Вселенные» в cpdt ( http://adam.chlipala.net/cpdt/html/Universes.html ), который запускает Set Printing Universes. для просмотра дополнительных комментариев к типам. Однако я использую CoqIde 8.6, и это не дает никакого эффекта....