Вопросы с тегом Идрис

0 голосов

1 ответ

Есть ли в idris специальный синтаксис c для чистого ключевого слова?

Oneiros / 06 августа 2020

1 голос

1 ответ

Не удалось объявить интерфейс MonadPlus, ограниченный для Monad

ChessMax / 01 августа 2020

0 голосов

0 ответов

Могут ли количественные типы гарантировать сложность?

Joel Berkeley / 21 июня 2020

2 голосов

0 ответов

Как сопоставить все целые числа в диапазоне в общей функции?

Pavel Strakhov / 30 мая 2020

1 голос

1 ответ

Нецелые функции рассматриваются как константы на уровне типа?

Joel Berkeley / 28 мая 2020

1 голос

1 ответ

Функция Идриса получает ошибку несоответствия типа

Oneiros / 26 мая 2020

2 голосов

1 ответ

Как Prelude позволяет использовать литералы numeri c для Nat?

Joel Berkeley / 05 мая 2020

1 голос

1 ответ

Проверка типов для Векторов в Идрисе

geguze / 04 мая 2020

0 голосов

2 ответов

ошибка реального пути с Chez Scheme при установке Idris2

iluvAS / 03 мая 2020

0 голосов

1 ответ

Команды поиска / поднятия дыры Idris для Emacs

Javier / 29 апреля 2020

7 голосов

1 ответ

Об определении «многопараметрических» функций путем частичного применения в Haskell -подобных языках

kostrikin-buh / 22 апреля 2020

2 голосов

1 ответ

Идрис: доказательство о конкатенации векторов

LorenzoPerticone / 20 апреля 2020

1 голос

1 ответ

Тензорное определение с произвольно вложенными Vects

Joel Berkeley / 12 апреля 2020

1 голос

1 ответ

Идрис передает доказательство функции, что аргументы являются LTE

Most Wanted / 12 апреля 2020

1 голос

1 ответ

Как убедить Идриса в длине вектора

Haspemulator / 06 апреля 2020

0 голосов

0 ответов

Как установить привязки для пакета SDL и Draw в Idris

OldTom / 03 апреля 2020

0 голосов

1 ответ

Соответствие шаблону Идриса на преемнике (следующее значение)

renanreismartins / 03 апреля 2020

1 голос

0 ответов

Почему несвязанные имплики недействительны, когда находятся в положении функции?

Joel Berkeley / 30 марта 2020

2 голосов

0 ответов

Как доказать, что 2 является Prime в Идрисе?

yanos / 28 марта 2020

1 голос

1 ответ

Сопоставление образцов на продуктах в Идрисе

Arka Ghosh / 25 марта 2020

0 голосов

0 ответов

Почему Идрис считает этот случай невозможным?

Ganesh Sittampalam / 24 марта 2020

0 голосов

1 ответ

Можно ли избежать явного сброса недопустимых дел в полных функциях в Idris?

Ganesh Sittampalam / 21 марта 2020

1 голос

1 ответ

Интерактивные команды редактирования Idris не работают в Atom на Linux

OldTom / 16 марта 2020

1 голос

1 ответ

Как передать функцию через пользовательский Idris FFI?

Nick Tchayka / 15 марта 2020

1 голос

0 ответов

Идрис не распознает эквивалентные типы

Charlie Gunn / 12 марта 2020