В Haskell я мог бы реализовать if следующим образом: if' True x y = x if' False x y = y spin 0 = () spin n = spin (n - 1) Это ведет себя так, как я ожидаю : haskell> if' True (spin 1000000) () -- takes a moment haskell> if'...

В последнее время я имел роскошь немного изучить Идрис, и одна вещь, которую я нашел чрезвычайно удобной, — это !-нотация, которая позволяет мне сокращать монадический код внутри блока do, такого как a' <- a b' <- b c' <- c someFunction...

Раздел учебника по where предложениям содержит 2 условия. за возможность опустить объявление типа функции f в предложении where : f появляется в правой части определения верхнего уровня. Тип f можно полностью определить с...

Можно ли в Идрисе переписать все функции с помощью " с помощью «использовать case» вместо «with»? Если нет, не могли бы вы привести контрпример?

Я новичок в Idris и пытаюсь уловить основные понятия и синтаксис. Даже если это может показаться бессмысленным, я пытаюсь определить функцию half , которая вдвое уменьшает натуральное число. Я хочу придумать что-то вроде: half : (n : Nat)...

То есть существует ли центральный репозиторий пакетов программного обеспечения с открытым исходным кодом, написанного на Idris? Некоторое гугление привело меня на страницу idris-hackers на github, здесь . А еще я могу поискать проекты на гитхабе,...

В следующем коде Idris> :t \x => x + x \x => x + x : Integer -> Integer Idris выводит тип Integer для переменной x, где я думаю, что он должен выводить ограничение интерфейса, как в Haskell: Haskell> :t (\x y -> x + y)...

По сути, я хочу доказать, что либо n - m , либо m - n равны нулю в рекурсивной арифметике. Для этого я безуспешно пытался использовать шаблон rewrite ... in ... . Ниже приведен базовый код: data Natural = C | S Natural resta : Natural...

Это кажется невозможным для извлечения второго элемента сигмы по исчислению конструкций. Более того, похоже, что не существует известного простого способа расширить исчисление конструкций с зависимыми исключениями без потери согласованности. Таким...

Я изучаю Идрис, и у меня есть небольшой вопрос для новичков. Я выполняю упражнение 2 из главы 8.3 книги по разработке с использованием Idris. Дело в том, чтобы реализовать DecEq для вашего собственного Vector . Вот как далеко я зашел: data...

Следующие определения типов Idris проверяются с помощью Idris 1.3.0: foo : (xs : List Nat) -> xs = ([] <+> xs) foo xs = Refl однако это не так: foo : (xs : List Nat) -> xs = (neutral <+> xs) foo xs = Refl дает...

Предположим, мы хотели бы иметь «правильный» minus для Nat s, требуя m <= n для n `minus` m , чтобы иметь смысл: %hide minus minus : (n, m : Nat) -> { auto prf : m `LTE` n } -> Nat minus { prf = LTEZero } n Z = n minus { prf =...

Я пытаюсь написать тестовый код, чтобы проверить, действительно ли plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a доказывает a + b = b + a на натуральных числах, то есть код не подделывает их, используя типизированные отверстия,...