idris

2зной

1ответ

Именованные реализации - Почему @ {myOrd} помещается перед параметрами?

В следующем коде, почему @{myOrd} размещен перед его параметрами, а не после? [myOrd] Ord Nat where compare Z (s n) = GT compare (S n) Z = LT compare (z z = EQ compare (S x) (S y)

4зной

2ответ

Как отменить HVect в Идрисе?

Я новичок в Irdis. Можно ли перевернуть HVect? Если я назову реверс на HVect [String, Int], он должен вернуть HVect [Int, String], и если я вызову реверс на HVect [String, Int, Day], он должен вернуть

2зной

1ответ

Понимание `к: Nat ** 5 * к = n` Подпись

Следующая функция компилируется: onlyModByFive : (n : Nat) -> (k : Nat ** 5 * k = n) -> Nat onlyModByFive n k = 100 Но что k представляет с синтаксисом Nat ** 5 * k = n? Также, как я могу назвать э

7зной

1ответ

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

В настоящее время я изучаю проверку модели (модальная логика, LTL, CTL, SAL model checker и т. Д.), И в свободное время я изучаю Idris, который является строго типизированным функциональным языком про

0зной

1ответ

Как определить все субразмеры HVect?

Я хотел бы определить все подразмеры HVect как HVect. Пример: import Data.HVect myHVect : HVect [Int, String, List Nat] myHVect = [42, "text", [1, 2, 3]] subDimensions : HVect [ HVect [Int], HVec

1зной

1ответ

Helper Функция определить, если Nat `mod` 5 == 0

Xash дала мне полезный ответ на Function to Determine if Nat is Divisible by 5 at Compile-Time (что я переименовал от моего первоначального длинного имени): onlyModBy5 : (n : Nat) -> n `modNat` 5 = 0

1зной

1ответ

Определить, равномерна ли сумма очков Vect n Nat's 5?

Cactus продемонстрировал, как ответить на мой вопрос: Helper Function to Determine if Nat `mod` 5 == 0. Он писал: onlyModBy5 : (n : Nat) -> {auto prf : n `modNat` 5 = 0} -> Nat onlyModBy5 n = n Зат