Вопросы по теме 'idris'
Что означает *** CPSZ: в журнале сборки Кабала при строительстве Идриса?
В настоящее время я строю Идрис через cabal install idris . В ответ на вывод:
Redirecting build log to {handle:/home/me/.cabal/logs/idris-0.9.14.3.log}
Я решил отслеживать сборку с помощью tail -f /home/me/.cabal/logs/idris-0.9.14.3.log ....
110 просмотров
schedule
13.05.2022
Векторы Идриса против связанных списков
Проводит ли Идрис какую-либо оптимизацию под капотом векторов? Потому что, судя по всему, вектор Идриса - это просто связанный список с известным размером (известным во время компиляции). Фактически, в целом кажется, что вы могли бы выразить...
1289 просмотров
schedule
14.02.2022
Экземпляр VerifiedMonad для монады ошибки
Я пытаюсь завершить доказательство monadLeftIdentity для следующего типа данных:
data ErrorM : (a : Type) -> Type where
AllGood : a -> ErrorM a
Error : String -> ErrorM a
instance Monad ErrorM where
(AllGood x) >>= f = f x...
135 просмотров
schedule
28.08.2022
Сделать один аргумент больше другого в Idris
Я пытаюсь написать функцию mSmallest , которая принимает два натуральных числа, n и m в качестве входных данных, и создает вектор. Выходной вектор содержит m наименьших членов конечного набора с n элементами.
Например, предполагается, что...
267 просмотров
schedule
27.07.2023
Примитивные операции в доказательствах
Для изучения зависимых типов я переписываю свою старую игру на Haskell в Idris. В настоящее время «движок» игры использует встроенные целочисленные типы, такие как Word8 . Я хотел бы доказать некоторые леммы, касающиеся числовых свойств этих чисел...
193 просмотров
schedule
04.06.2023
Действительно ли Идрис строго оценивается?
Исходя из Haskell, я читал историю Идриса о лени (нестрогости). Я просмотрела последние примечания к выпуску и нашла код , похожий на следующий
myIf : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a
myIf True t e = t
myIf False t e = e...
838 просмотров
schedule
12.12.2023
Символ Idris FFI не найден
В последнее время я возился с Idris и решил попробовать поиграть с его Network.Socket библиотекой. Я запустил REPL, импортировал модуль и создал сокет с помощью команды socket . При попытке выполнить операцию IO я столкнулся со следующей...
179 просмотров
schedule
16.08.2022
Идрис - Невозможно оценить приложение функции в типе
У меня проблема, когда у меня есть значение типа fun a , где fun является функцией, а a значением, которое не вычисляется при проверке типа и выдает ошибку объединения, когда я заставляю его быть результатом этой функции применение....
223 просмотров
schedule
25.05.2022
Простой преобразователь температуры с зависимым типом в Haskell, можно ли сделать этот код короче?
Функция convert ниже имеет сигнатуру типа:
SUnit fromUnit-> SUnit toUnit ->Value fromUnit -> Value toUnit ,
который имеет избыточность , поскольку одна и та же информация может быть выражена с помощью:
Value fromUnit ->...
204 просмотров
schedule
08.06.2024
Есть ли функция по модулю в idris?
В Haskell есть функции mod и rem . Существуют ли аналогичные функции в Idris, особенно определенные для Nat ?
570 просмотров
schedule
19.05.2023
Автоматический неявный аргумент перестает работать, когда типу присваивается имя
При написании этого ответа я заметил, что пока это работает как положено:
onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat
onlyModBy5 n = n
foo : Nat
foo = onlyModBy5 25
но как только я даю имя свойству, оно перестает...
43 просмотров
schedule
18.04.2023
Странная синтаксическая ошибка
data A = B | C Int
implementation Semigroup A where
B <+> x = x
x <+> B = x
C m <+> C n = C (m + n)
дает мне синтаксическую ошибку
./Nodes/Test.idr:3:1: error: expected: ";",
"|", declaration, end of input...
94 просмотров
schedule
09.12.2023
Ограничение входных аргументов функцией
Допустим, я хочу определить функцию Фибоначчи как следующую функцию:
fibo : Int -> Int
fibo 1 = 1
fibo 2 = 2
fibo n = fibo (n-1) + fibo (n-2)
Эта функция, очевидно, не является полной, поскольку она не определена для целых чисел ниже 1,...
121 просмотров
schedule
17.04.2023
Как закодировать возможные переходы состояний в типе?
Я пытаюсь воспроизвести в Haskell этот фрагмент кода Idris, который обеспечивает правильную последовательность действий через типы:
data DoorState = DoorClosed | DoorOpen
data DoorCmd : Type ->
DoorState ->
DoorState...
358 просмотров
schedule
27.09.2022
Где полезен оператор Idris ==?
Как новичок в программировании, управляемом типами, мне интересно использовать оператор == . Примеры демонстрируют, что недостаточно доказать равенство между двумя значениями определенного типа, и для конкретных типов данных вводятся специальные...
102 просмотров
schedule
15.06.2023
Идрис: Неявные параметры в записях
Когда я пытаюсь скомпилировать этот пример
record R where
f: () -> {t: Type} -> t
Я получаю эту ошибку:
Type mismatch between
() -> t1 (Type of f)
and
() -> t (Expected type)
Specifically:
Type...
159 просмотров
schedule
13.01.2024
Отслеживание состояния при написании доказательств равенства, которые представляют собой длинные цепочки транзитивно связанных шагов
Я писал в Идрисе следующее доказательство:
n : Nat
n = S (k + k)
lemma: n * n = ((k * n) + k) + (1 + (((k * n) + k) + 0))
lemma = sym $
rewrite plusZeroRightNeutral ((k * n) + k) in
rewrite plusAssociative ((k * n) + k) 1 ((k *...
103 просмотров
schedule
27.08.2022
Функция работает только при переворачивании
Почему ошибка?
import Data.Vect
import Data.Vect.Quantifiers
get : (i : Fin n) -> All (flip Vect t) ls -> Vect (index i ls) t
get FZ (y :: z) = y
get (FS y) (z :: w) = get y w
nproject : Vect l (n : _ ** Fin (index n ls)) -> All (flip...
57 просмотров
schedule
14.04.2024
жирная стрела в Идрисе
Я надеюсь, что этот вопрос уместен для этого сайта, он просто о выборе конкретного синтаксиса в Idris по сравнению с Haskell, поскольку оба они очень похожи. Думаю, это не так важно, но мне очень любопытно. Идрис использует => в некоторых...
178 просмотров
schedule
15.01.2024
Lightyear requireFailure не выполняет откат
Я хочу разобрать серию любых 4 символов. Однако эти символы не должны формировать определенную строку ( "bb" в примере ниже). Итак, "aaaa" и "abcd" в порядке, но ни "bbcd" , ни "abbc" не должны совпадать.
Я составил следующий парсер:...
64 просмотров
schedule
18.04.2023
