Вопросы с тегом зависимый-тип

2 голосов

1 ответ

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

Eayus / 02 августа 2020

6 голосов

4 ответов

Разворачивание экзистенциально количественно оцененного GADT

Poscat / 20 июня 2020

7 голосов

1 ответ

Как в scala указать компилятору реализовать эквивалентность двух абстрактных типов?

tribbloid / 19 июня 2020

7 голосов

1 ответ

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

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

1 голос

1 ответ

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

jmite / 14 апреля 2020

2 голосов

0 ответов

Как можно объяснить две эти-эквивалентные программы agda с различным поведением?

Warrick Macmillan / 03 апреля 2020

0 голосов

0 ответов

Как правильно определить запись с параметрами в Agda?

Xavier Ripoll / 10 марта 2020

2 голосов

2 ответов

Индукция на уровне типа в KnownNats: перекрывающиеся экземпляры

gilgamec / 20 февраля 2020

0 голосов

0 ответов

Идрис невозможное ключевое слово доказывает неправильное предложение

12412316 / 12 февраля 2020

3 голосов

1 ответ

Агда: могу ли я доказать, что типы с разными конструкторами не пересекаются?

jmite / 12 января 2020

Для получения более полной информации посмотрите в списке вопросов или в популярных тегах.

...