Вопросы с тегом agda

0 голосов

1 ответ

Назначение анонимных модулей в Agda

MrO / 07 августа 2020

1 голос

1 ответ

Почему я не могу переместить частичное определение блока в локальную привязку?

Cactus / 07 августа 2020

1 голос

1 ответ

Импорт Cubical.Data.Nat прерывает isOfHLevel → isOfHLevelDep

Cactus / 05 августа 2020

1 голос

0 ответов

Установка Agda на windows

Chetan Vuppulury / 03 августа 2020

2 голосов

1 ответ

Предикат Бове-Капретты в опоре

Eayus / 02 августа 2020

0 голосов

1 ответ

Понимание сбоев рекурсивных вызовов на простом доказательстве FSA и обычных языков в Agda

Warrick Macmillan / 17 июня 2020

3 голосов

1 ответ

Как можно использовать исключение идентичности (в agda), чтобы доказать Экман-Хилтон для путей более высокой размерности в HoTT?

Warrick Macmillan / 28 мая 2020

0 голосов

1 ответ

Понимание проблем вывода типов в agda при проверке законов применения функций basi c

Warrick Macmillan / 27 мая 2020

1 голос

1 ответ

Убедить Agda в том, что рекурсивная функция завершается

DoppeDee / 09 мая 2020

0 голосов

1 ответ

Как загрузить и настроить стандартную библиотеку для Agda в Ubuntu?

J.Lili / 29 апреля 2020

2 голосов

1 ответ

Покрытие для бинарных натуралов как высший индуктивный тип

Patrick Stevens / 28 апреля 2020

4 голосов

1 ответ

Использование Agda "переписать", чтобы доказать "композиция карт является карта композиций"

funemy / 28 апреля 2020

2 голосов

2 ответов

Как определить пользовательский принцип индукции в coq?

Warrick Macmillan / 27 апреля 2020

1 голос

2 ответов

Кубическая Агда: как мне доказать две вещи не равные

Patrick Stevens / 26 апреля 2020

1 голос

1 ответ

Как явно использовать принцип индукции в coq?

Warrick Macmillan / 26 апреля 2020

2 голосов

1 ответ

Где находится _≡⟨_⟩_ стандартная библиотека Agda?

kkshinkai / 20 апреля 2020

7 голосов

1 ответ

Производные структур данных в Агде

N. Brett / 15 апреля 2020

1 голос

1 ответ

Работа в рамках решимости Agda

Warrick Macmillan / 14 апреля 2020

1 голос

1 ответ

Взаимно индуктивные описания с разными типами индексов?

jmite / 14 апреля 2020

4 голосов

1 ответ

Является ли эта формулировка по модулю набора?

Cactus / 12 апреля 2020

0 голосов

1 ответ

Переводить определения Coq в agda?

Warrick Macmillan / 10 апреля 2020

1 голос

2 ответов

Как можно использовать с проверять в Агде?

Warrick Macmillan / 10 апреля 2020

2 голосов

1 ответ

Agda не позволит мне заполнить типизированное отверстие термином соответствующего типа из-за ограничения определения равенства

TAH / 08 апреля 2020

1 голос

0 ответов

Как отладить рекурсор вычитания, который проверяет правильность, но не может быть подтвержден в agda?

Warrick Macmillan / 06 апреля 2020

1 голос

1 ответ

Как определить функцию диапазона для отношения в Agda (теория множеств)

helq / 05 апреля 2020