idris

8зной

4ответ

Где и почему следует использовать дополнительные пустые шаблоны?

Например: intersectBy : (a -> a -> Bool) -> List a -> List a -> List a intersectBy _ [] _ = [] intersectBy _ _ [] = [] intersectBy eq xs ys = [x | x <- xs, any (eq x) ys] Есть дополнительные шаб

5зной

1ответ

natToFin, когда есть доказательства того, что преобразование будет работать

natToFin В функции из стандартной библиотеки имеет следующую подпись: natToFin : Nat -> (n : Nat) -> Maybe (Fin n) natToFin 4 5 возвращается Just (FS (FS (FS (FS FZ)))) : Maybe (Fin 5), в то время к

3зной

1ответ

Определение категорий в Idris

Я пытаюсь определить проверенные категории, внутренние для типов Idris, но мой подход не вводит проверку. class Cat ob (mor : ob -> ob -> Type) where comp : {a : ob} -> {b : ob} -> {c : ob} -> mo

1зной

1ответ

Confused о промежуточном типе в Idris

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

3зной

1ответ

Простые числа Идриса

В Идриса 0.9.17.1, с вдохновением от https://wiki.haskell.org/Prime_numbers, Я написал следующий код для генерации простых чисел module Main concat: List a -> Stream a -> Stream a concat [] ys = ys

2зной

1ответ

Есть ли что-то более информативное, чем: set showimplicits для дешифровки сбоев унификации?

Есть ли что-то более информативное, чем: set showimplicits для отслеживания ошибок унификации? В настоящее время я получаю это и не знаю, куда идти отсюда:

6зной

1ответ

Доказательство законов функтора потока

Я писал что-то похожее на поток. Я могу доказать каждый функтор закон, но я не могу придумать, как доказать, что это всего: module Stream import Classes.Verified %default total codata MyStream a