Описание тега agda-mode
Agda - это функциональный язык программирования с зависимой типизацией: он имеет индуктивные семейства, похожие на GADT в Haskell, но их можно индексировать по значениям, а не только по типам. Чтобы использовать Agda в таких редакторах, как Emacs или Atom, вам необходимо включить / настроить редактор в режиме agda.
1
ответ
Агда режим в аквамаке
Я не могу заставить работать режим Agda на Aquamacs. Я использую macOS Sierra. Agda версии 2.5.4 и Aquamacs 3.3 Вот что я получаю, когда запускаю команды agda-mode agda-mode setup It seems as if setup has already been performed. agda-mode locate /us…
07 июн '18 в 21:08
0
ответов
Agda: привязки emacs в командной строке?
Можно ли использовать некоторые функции, которые agda связывает с emacs, и переносить их в командную строку? Есть ли в командной строке agda опции для работы с дырами? C-c C-,, C-c C-dили введите отчисления типа C-c C-d?
22 фев '19 в 06:53
1
ответ
Как проверить, основывается ли термин agda, связанный с конкретным именем, на дыре?
Для целей сценария я хотел бы запросить agda-компилятор об определении функции в исходном файле agda. Я хотел бы задать вопрос: функция, названная X, полагается на дыру или нет? (т.е. это "законченное доказательство" или "доказательство в процессе")…
09 ноя '17 в 03:35
2
ответа
Agda: Не удается найти std-lib при установке с помощью стека
Я пытаюсь скомпилировать файл Agda, но у меня не получается найти стандартную библиотеку. Я видел документацию здесь. Я использовал Stack для его установки: > which agda /home/joey/.local/bin/agda И я установил переменную окружения для моего ката…
27 окт '17 в 21:51
1
ответ
Понимание практического экзамена об Агде
Я прохожу практический экзамен по языковым фондам программирования с использованием agda, и у меня есть следующий вопрос: Вам выдается следующая декларация Агды: data Even : N → Set where ezero : Even 0 esuc : { n : N } → Even n → Even (2+ n) Предпо…
06 мар '17 в 05:15
1
ответ
Как установить agda-mode на OSX El Capitan?
Я пытаюсь установить agda-mode на OSX. Я следовал официальному руководству (попробовал несколько других тоже), но не могу заставить его работать. При загрузке Emacs/Aquamacs я получаю следующую ошибку: Warning (initialization): An error occurred whi…
25 апр '16 в 23:14
0
ответов
Руководство по очень мелкому встраиванию VHDL в AGDA, часть II
Привет, я задал вопрос, касающийся моего проекта, я работал над ним и добился следующих успехов: module project1 where open import Data.Empty open import Data.Unit hiding (_≟_) open import Data.Nat hiding (_≟_; _⊔_) open import Data.String open impo…
23 апр '17 в 21:28
0
ответов
Руководство по очень мелкому встраиванию VHDL в AGDA
Для моего проекта в Языки программирования я делаю очень поверхностное и простое встраивание цифровых схем VHDL в agda. Цель состоит в том, чтобы написать синтаксис, статическую семантику, динамическую семантику, а затем написать некоторые доказател…
17 апр '17 в 14:23
1
ответ
Как я могу использовать agda2-mode для генерации паттернов, когда ожидаю увидеть абсурдный паттерн?
Например, мы доказываем 2 + 2 != 5: data _+_≡_ : ℕ → ℕ → ℕ → Set where znn : ∀ {n} → zero + n ≡ n sns : ∀ {m n k} → m + n ≡ k → suc m + n ≡ suc k И я могу доказать это вручную: 2+2≠5 : 2 + 2 ≡ 5 → ⊥ 2+2≠5 (sns (sns ())) Но я хочу шаблон (sns (sns ()…
06 ноя '17 в 17:54
1
ответ
Как мне ввести "·" (средняя точка) в режиме агда?
Я работаю через документ, который использует символ средней точки в коде Agda. Я хотел бы иметь возможность печатать его без копирования / вставки. Как я могу войти в него с agda-mode? Я пробовал типичные ресурсы, такие как http://agda.readthedocs.i…
12 июн '16 в 03:15
2
ответа
Агда: вернуть голову и хвост пустого списка
Я изучаю агду и практикуюсь в списках, чтобы лучше понять. Прямо сейчас я пытаюсь написать функции для списка. Я запутался в том, как вернуть голову и хвост пустому списку. Вот мой код: data list (A : Set) : Set where [] : list A _∷_ : A → list A → …
16 фев '17 в 21:22
2
ответа
Как мне набрать m≤n в режиме Agda Emacs без превращения его в m into?
Каков лучший способ напечатать что-то вроде m≤n в режиме Agma Emacs? Если я наберу m \ < = n, я получу m≰, что раздражает. Мой текущий обходной путь - набрать m \ < = Space Backspace n, но он не очень эргономичен. Есть ли что-то, что я могу сделать,…
21 май '19 в 22:40
1
ответ
Вызов функции в Агде
У меня есть этот код, который в основном представляет собой hello world, с функцией добавления, он компилирует и запускает и выводит "Hello, world 5!": open import Common.IO data ℕ : Set where zero : ℕ suc : ℕ → ℕ -- how to call a function in agda i…
26 мар '19 в 15:06
0
ответов
Emacs не реагирует, когда я нажимаю C-. (Точка / период)
Я учу Агду и когда набираю Cc C-. в моем Emacs нет никакой реакции. Я могу напечатать любой Cc . или Cc M-. и тогда мне скажут, что эти привязки не определены. Но когда я пытаюсь набрать Cc C-. мини-буфер показывает только C-c и похоже, что Emacs жд…
10 июн '19 в 09:33
1
ответ
Ошибка отсутствующей подписи типа в Agda, которую я не знаю, как избежать
У меня есть следующий код в файле trial_agda.agda в emacs: module trial_agda where data : Set where zero : suc : → _+_ : → → zero + n = n (suc n) + n′ = suc (n + n′) Он производит /Users/myname/trial_agda.agda:8,1-13 Missing type signature for left …
10 ноя '19 в 16:59
1
ответ
Загрузка файлов в Agda: неясное объяснение в Learn you an Agda
Я сделал файл emacs trial_agda.agda со следующим кодом: module trial_agda where data : Set where zero : suc : → data _even : → Set where ZERO : zero even STEP : ∀ x → x even → suc (suc x) even _+_ : → → (zero + n) = n (suc n) + n′ = suc (n + n′) В h…
10 ноя '19 в 19:45
1
ответ
Подсветка синтаксиса для Agda-mode 2 в Doom Emacs
Мне нужна помощь в настройке режима agda для работы в моей системе emacs. По сути, подсветка синтаксиса происходит только после сохранения, а не в реальном времени, как в других стандартных режимах. Я сделал базовый урок. Я запускаю Manjaro в своей …
02 мар '20 в 09:19
0
ответов
Непонятная лексическая ошибка при компиляции файла Agda
(Здравствуйте, заранее спасибо) Я работаю над введением в HoTT в agda https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html и начал свой собственный проект Agda (2 файла, вряд ли проект), когда я работаю над конспектами лекции, одн…
26 ноя '19 в 06:55
1
ответ
Agda - Интерактивное построение доказательств - Как использовать синтаксис дыр?
Извините за странное название, я понятия не имею, как на самом деле названы эти концепции. Я слежу за Agdaучебник и есть раздел, объясняющий, как индуктивно строить доказательства: https://plfa.github.io/Induction/ Довольно здорово, что вы можете ша…
14 май '20 в 13:35
1
ответ
Предотвращение того, чтобы разработка agda нарушила использование базовой стандартной библиотеки?
Я работаю с разрабатываемой версией agda, которая сейчас несовместима с базовой стандартной библиотекой версии 1.3. wmacmil@w:~/.agda$ agda --version Agda version 2.6.2-41b6b25 Базовый файл failure.agda, module failure where open import Data.String …
18 сен '20 в 01:33