我可以寫函數 powApply : Nat -> (a -> a) -> a -> a
powApply Z f = id
powApply (S k) f = f . powApply k f
，並證明平凡： powApplyZero : (f : _) -> (x : _) -> powApp Z f x = x
powApplyZero f x = Refl
到目前爲止，一切都
像下面的表達式是非常有效的在伊德里斯： let x = Just 5 in let y = Just 6 in [|x/y|]
有人能寫出像下面的表達式？ let x = Just 5 in let y = Just 6 in [| if x == 0 then 0 else y|]
我似乎無法得到它編譯。
人們可以在伊德里斯函數返回一個類型，例如 t : Type -> Type -> Type
t a b = a -> b
但是現在的情況上來，我想用->摺疊類型列表（用寫一些解析器實驗時），即 typeFold : List Type -> Type
typeFold = foldr1 (->)
這樣typeFold [String, Int]會給String -> Int : Typ
我試圖讓人們可以稱之爲伊德里斯的可判斷的分析器。起初我只是在分析自然數，但遇到了意想不到的問題。產生它的代碼的最小例子是這樣的： data Digit : Char -> Type where
Zero : Digit '0'
One : Digit '1'
digitToNat : Digit a -> Nat
digitToNat Zero = 0
digitToN
類型謂詞生成運行時證明我使用此類型推理可以在其上進行可判定的解析字符串： data Every : (a -> Type) -> List a -> Type where
Nil : {P : a -> Type} -> Every P []
(::) : {P : a -> Type} -> P x -> Every P xs -> Every P (x::xs)
例如，
我是新來的依賴類型，並且擁有Haskell的經驗，我正在慢慢地學習Idris。爲了鍛鍊，我想寫一個霍夫曼編碼。目前我正試圖寫一個證明，即代碼樹的「扁平化」產生一個前綴代碼，但已經與量詞卡住了。 我有一個簡單的感性主張，一個列表是一個又一個的前綴： using (xs : List a, ys : List a)
data Prefix : List a -> List a -> Type
阿格達利用以下操作來套之間表現出相反： _↔_ : ∀ {f t} → Set f → Set t → Set _
是否有伊德里斯等效？我試圖定義列表上的袋子平等 data Elem : a -> List a -> Type where
Here : {xs : List a} -> Elem x (x :: xs)
There : {xs : List a} -> El
我正在爲foo一個未解metavariable在下面的代碼： namespace Funs
data Funs : Type -> Type where
Nil : Funs a
(::) : {b : Type} -> (a -> List b) -> Funs (List a) -> Funs (List a)
data FunPtr : Funs a