根據https://homes.cs.washington.edu/~jrw12/InductionExercises.html我試圖證明sum和sum_cont是等價的。我到： sum : List Nat -> Nat
sum [] = 0
sum (x :: xs) = x + sum xs
sum_cont' : {a : Type} -> List Nat -> (Nat ->
我預計今年以評估3，但得到了一個錯誤，而不是： Idris> :let x = Just 2
Idris> 1 + !x
(input):1:3-4:When checking an application of function Prelude.Interfaces.+:
Type mismatch between
Integer (Type of (_bindA
我試圖執行以下操作： headEqual : DecEq a => (x : a) -> (y : a) -> Maybe (Dec (x = y))
headEqual x y = case decEq x y of
Yes Refl => Just (Yes Refl)
No contra => Nothing
vectEqual : DecEq a
在我探索伊德里斯的旅程中，我試圖用「慣用」的方式編寫一個小日期處理模塊。這是我到目前爲止。 首先，我有一些基本的類型來表示天，月，年： module Date
import Data.Fin
Day : Type
Day = Fin 32
data Month : Type where
January : Month
February : Month
.
當我打開這個文件： %default total
data Parity = Even | Odd
opposite: Parity -> Parity
opposite Even = Odd
opposite Odd = Even
data PNat : Parity -> Type where
PZ : PNat Even
PS : PNat p -> PN
我希望能夠說，對於簽名t-> t的f的函數，對於t中的所有x，f（f（x））= x。 當我運行此： %default total
-- The type of parity values - either Even or Odd
data Parity = Even | Odd
-- Even is the opposite of Odd and Odd is the opposite
我定義我自己的Vect數據類型如下 data MyVect : (n : Nat) -> (t : Type) -> Type where
Nil : MyVect Z t
(::) : (x : t) -> (xs : MyVect n t) -> MyVect (S n) t
然後開始實施的數據類型 Foldable MyVect where
foldr =