idris

8熱度

1回答

我如何讓Idris自動證明兩個值不相等？

我如何讓Idris自動證明兩個值不相等？ p : Not (Int = String) p = \Refl impossible 我該如何讓Idris自動生成此證明？ auto似乎不能證明涉及Not的陳述。我的最終目標是讓Idris自動證明矢量中的所有元素都是唯一的，並且兩個矢量不相交。 namespace IsSet data IsSet : List t -> Type whe

proof idris 2017-09-30

---

2熱度

1回答

這個'with'塊爲什麼會破壞這個函數的整體性？

我試圖計算奇偶校驗與半的地板一起，在自然數： data IsEven : Nat -> Nat -> Type where Times2 : (n : Nat) -> IsEven (n + n) n data IsOdd : Nat -> Nat -> Type where Times2Plus1 : (n : Nat) -> IsOdd (S (n + n)) n

idris termination totality 2017-10-04

---

3熱度

1回答

伊德里斯改寫不會發生

import Data.Vect import Data.Vect.Quantifiers sameKeys : Vect n (lbl, Type) -> Vect n (lbl, Type) -> Type sameKeys xs ys = All (uncurry (=)) (zip (map fst xs) (map fst ys)) g : {xs,ys : Vect n (

idris 2017-10-04

---

4熱度

1回答

伊德里斯 - 感性步

證明考慮下面的函數 tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber) tryMove Z from to [] = Nothing tryM

idris 2017-10-06

---

1熱度

1回答

如何在Idris中編寫一個非常懶惰的版本？

inf : Nat inf = S inf minimum' : Lazy Nat -> Lazy Nat -> Lazy Nat minimum' Z b = Z minimum' b Z = Z minimum' (S a) (S b) = S (minimum' a b) main : IO() main = do print $ Force $ minimum'

idris 2017-10-10

---

6熱度

1回答

爲什麼idris中的這兩個元組相等？

我讀Type driven development with Idris，和的一個練習要求讀者限定，使得隨着一個矢量可以表示一個類型TupleVect，： TupleVect 2 ty = (ty, (ty,())) 我解決它通過定義以下類型： TupleVect : Nat -> Type -> Type TupleVect Z ty =() TupleVect (S k) ty = (

idris 2017-10-19

---

3熱度

1回答

伊德里斯 - 懶惰的評價問題

考慮此程序： module test import Effects import Effect.StdIO (>>==) : Maybe a -> Lazy (a -> Maybe b) -> Maybe b (>>==) Nothing (Delay map) = Nothing (>>==) (Just x) (Delay map) = map x nothing : Str

monads lazy-evaluation idris 2017-10-19

---

2熱度

1回答

隱式參數的順序如何影響idris？

這種失敗： > the ({A : Type} -> A -> {B : Type} -> B -> (A, B)) MkPair (input):1:5:When checking argument value to function Prelude.Basics.the: Type mismatch between A -> B1 -> (A, B1) (Type

idris 2017-10-21

---

1熱度

1回答

難度在伊德里斯

我試圖在我的定義的數據類型中的一種證明屬性如下應用證明： reverseProof' : (inputBlock : Block iType iSize iInputs) -> (ind : Fin rSize) -> (rInputs : Vect rSize Ty) -> (receiveBlock : Block rType rSize rInput

idris theorem-proving 2017-09-11

---

3熱度

1回答

伊德里斯：在記​​錄隱參數

當我嘗試編譯這個例子 record R where f:() -> {t: Type} -> t 我得到這個錯誤： Type mismatch between () -> t1 (Type of f) and () -> t (Expected type) Specifically: Type mismatch between

idris 2017-09-16

---