Описание тега proof-general
Proof General is a generic front-end for proof assistants, based on Emacs.
0
ответов
Tabbing дает ошибку в доказательстве general/emacs
У меня есть emacs 23.3.1 на Ubuntu 12.04 LTS, с общим доказательством 4.2. При редактировании файлов coq в режиме "coq Holes" (который используется по умолчанию, когда я хакую coq), я не могу перейти. Это дает ошибку неверный тип аргумента целое-или…
29 июл '15 в 10:04
1
ответ
Как настроить цвета для Command и Tactic в ProofGeneral при использовании Coq в Emacs?
Я хочу раскрасить какую-то конкретную команду и тактику в другой цвет, например, я хочу, чтобы команды "Печать" и "Найти" были серыми, а "индукция" - каким-то особым цветом, отличным от других тактик. Возможно ли это в ProofGeneral? Если это не наст…
09 окт '18 в 03:08
0
ответов
Определение моего собственного типа OrderedType в Coq
Чтобы попытаться понять, как определить свой собственный OrderedType в Coq я работаю над примерами OrderedTypeдано в стандартной библиотеке в Coq.Structures.OrderedTypeEx ( здесь). На данный момент я имею дело только с первой парой модулей: Require …
20 ноя '17 в 17:56
2
ответа
Агда-подобное программирование в Coq/Proof General?
В отличие от Agda, Coq стремится отделить доказательства от функций. Тактика, которую дает Coq, отлично подходит для написания доказательств, но мне интересно, есть ли способ воспроизвести некоторые функциональные возможности режима Agda. В частност…
24 янв '17 в 19:55
2
ответа
Как вы смотрите, где идентификаторы определены в Coq эффективно?
В большинстве IDE или текстовых редакторов вы можете щелкнуть правой кнопкой мыши термин, и он приведет вас к файлу, в котором этот термин определен. У CoqIDE этого нет, поэтому я занимаюсь coqdoc myfile.v --htmlЗатем перейдем к сгенерированным доку…
18 июл '15 в 18:34
3
ответа
Как отключить режим Verilog в emacs?
Я пытаюсь использовать CoQ с ProofGeneral, но встроенный режим Verilog тени *.v распознавание типов файлов. Можно ли как-то отключить его и позволить ProofGeneral переназначить их в режим coq?
08 мар '12 в 21:21
1
ответ
Как сказать Proof General, что ".csv"!= ".V"
Каждый раз, когда я открываю файл.csv в буфере Emacs, запускается Proof General (если он еще не запущен) и сбрасывает мои окна. Это действительно сбрасывает мою канавку Emacs и должно остановиться. Единственная часть моего init.el, которая имеет дел…
11 сен '15 в 21:52
1
ответ
Тензорный поток / Глубокий разум: как мне взять действия из наблюдений для математических алгоритмов, связанных с доказательствами?
Этот вопрос следует задать для получения указаний / предложений / помощи по использованию глубоководных библиотек с открытым исходным кодом: https://github.com/deepmind/lab или https://www.tensorflow.org/ в Python. Учтите, что я новичок в таких поня…
15 мар '17 в 11:55
1
ответ
Удалить стрелку в режиме Emacs ProofGeneral для Coq
Я использую ProofGeneral с Coq. Когда я делаю Cc C-return, Emacs выделяет область, обработанную Coq. Это мило. Тем не менее, он вставляет '=>' в следующую строку, которая перезаписывает первые два символа вашего ввода. Например, в настоящее время я …
18 окт '13 в 13:46
2
ответа
Isabelle2016 и Proof General
Я пытался научиться использовать Isabelle 2016. Хотя в принципе мне нравится идея асинхронной проверки корректности, мне не нравится Isabelle/jEdit по ряду причин, наиболее серьезной из которых является то, что она использует слишком много памяти (д…
21 фев '16 в 20:18
0
ответов
Как устранить ошибку импорта суффикса coq (физический путь привязан к логическому пути)
Вероятно, это вопрос новичка, но я не смог найти готовое решение, поэтому я буду просить здесь для справки. Версия Cocq 8.5pl2 Я пытался собрать coqfj. Первый make попытка не удалась с некоторой ошибкой в строке 37 в src/FJ/ClassTable.v, Этот вопр…
12 фев '17 в 08:19
1
ответ
Глифы Unicode для ключевых слов и операторов в Coq/Proof General под Emacs
Этот вопрос связан с настройкой режима Coq в Proof General в Emacs. Я пытаюсь, чтобы Emacs автоматически заменял ключевые слова и нотацию в Coq соответствующими глифами Unicode. Мне удалось определить fun быть греческой строчной лямбда λ, forall быт…
20 апр '12 в 18:14
0
ответов
Emacs работает в режиме Org и Coq в одном буфере
Мне нравится использовать Emacs для запуска ProofGeneral/Coq-mode, потому что интерактивный инструмент для проверки великолепен. Мне нравится использовать Emacs для запуска Org-режима, потому что это очень простой способ написать презентацию, в кото…
05 апр '18 в 18:30
2
ответа
Как управлять Emacs для разделения окна при интерпретации Coq
Я изучаю Coq с Emacs. Я пролил окно emacs вертикально, слева - документ, а справа - область редактирования кода. когда я интерпретирую программу Coq, результат отобразится в левом окне и покроет документ. Это беспокоит меня. Есть ли такой способ, ко…
17 сен '17 в 14:21
2
ответа
Невозможно предоставить длинные (более 1024 символов) входные данные для верхнего уровня OCaml и coqtop (и Proof General)
Изменить 4: Оказывается, что это на самом деле просто ограничение ввода TTY в целом; нет ничего конкретного в OCaml, Coq или Emacs, который вызывает проблему. Я работаю над программой Coq, использующей Proof General в Emacs, и обнаружил ошибку с вво…
04 июл '12 в 02:52
1
ответ
Курсор Emacs перепрыгивает перед точкой на Proof General
Я сталкиваюсь с этой проблемой только при запуске Proof General. Я предполагаю, что это какой-то случайный второстепенный режим, который запускается Proof General, но не могу понять, какой именно! Ниже приведен список второстепенных режимов на случа…
08 июл '15 в 09:30
1
ответ
Курсор Proof General скрывает мой код при использовании в терминале
Когда я использую emacs в оконном режиме, все выглядит нормально. Однако в терминале курсор Proof General (указывающий, где он находится в коде) скрывает первые два символа строки, в которой он находится. Это похоже на ошибку, но, возможно, это кака…
08 дек '15 в 22:28
1
ответ
Как отобразить скобки вокруг предположений в Isabelle/jEdit?
Когда цели отображаются Изабель в ProofGeneral, предположения представляются в виде квадратных скобок следующим образом: Однако в Isabelle/jEdit это, похоже, изменилось на стрелки мета-импликации: Хотя я понимаю, что первое несколько нестандартно, м…
11 апр '13 в 01:24
1
ответ
Как RegExp.exec заполняет массив результатов
Я играю с некоторыми регулярными выражениями и, глядя на некоторые из моих совпадений, мне стало интересно, почему функция exec дала столько же результатов, сколько и сама. Я просто ищу небольшое разъяснение о внутренней работе операции, чтобы мне б…
13 ноя '12 в 16:43
1
ответ
Настройте темную тему генерал-доказательства для Изабель
Я новичок как в Изабель, так и в Генерале Доказательств. Я пытаюсь установить темную тему в Proof General для использования с Изабель, но независимо от того, какую тему я выбираю (например, tango-dark, ample, monokaiи т. д.), нетронутый внутренний с…
19 фев '15 в 17:08