Я пытаюсь создать решающую функцию для типа, представляющего два последовательных элемента в...
У меня проблема может быть более общей, чем указано в вопросе.Я пытаюсь заставить работать...
В (* 1) можно прочитать следующее rewrite prf in expr Если у нас есть prf : x = y, а требуемый тип...
Я относительно новичок в idris и зависимых типах, и я столкнулся со следующей проблемой - я создал...
В Haskell мы можем сделать следующее, не получая ошибки времени выполнения ( ref ): mytake 0 _ = []...
Я работаю в небольшом проекте с целью дать определение Gcd, которое дает gcd из двух чисел вместе с...
Когда я пытаюсь это сделать в Idris, contrived : (List a, Char, (Int, Double), String, Bool) ->...
В неофициальном FAQ на официальной вики-странице Idris (официальной в том смысле, что она есть в...
Чтобы немного попрактиковаться с Idris, я пытался представить различные базовые алгебраические...
Я пытаюсь определить функцию (congruentialMethod) в Идрисе, которая среди прочего применяет...
Я играю с idris и пытаюсь реализовать расширяемые записи. Основная цель - гарантировать, что ключи...
Я пытаюсь улучшить свой навык Idris, взглянув на некоторые из упражнений Основы программного...
Я пытаюсь разделить доступную для записи память между потоками в idris, и я не могу этого сделать
Допустим, мы хотим доказать, что ослабление верхней границы Data.Fin не меняет значение числа
Я пытаюсь доказать, что после разбиения Vect на три части длина каждой части меньше, чем у...
ОБНОВЛЕНИЕ 3. Еще несколько попыток: $ curl -sSL https://get.haskellstack.org/ | sh Stack Version 1
Я пытаюсь узнать о зависимых типах в Идрисе, пытаясь что-то из моей глубины. Пожалуйста, потерпите...
В другом вопросе ( Как написать простую быструю сортировку на основе списка в Idris? ), мне...
В Haskell функции являются функторами, и следующий код работает как положено: (*3) `fmap` (+100) $...
В Haskell следующее выдает «hello»: putStrLn (['h', 'e', 'l',...
Я просто пытаюсь сделать минимум, чтобы перевести следующий Haskell на Idris (я не ищу...
Haskell позволяет: a:: Int a = 3 data MyList a = Nil | Cons a (MyList a) В то время как Идрис будет...
Скажем, у нас есть функция merge, которая просто объединяет два списка: Order : Type -> Type...
Я пытаюсь написать функцию начальных сегментов для векторов, которая хранит длину вектора как фин,...
Я хотел бы загрузить (двоичный) файл во время компиляции и сохранить его в переменной верхнего...