Test-Driven Development with Idris的第9章介紹了以下數據類型和removeElem函數。 import Data.Vect
data MyElem : a -> Vect k a -> Type where
MyHere : MyElem x (x :: xs)
MyThere : (later : MyElem x xs) -> MyEl
Type-Driven Development with Idris禮物： twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible
是對函數或值之上？如果它是前者，那麼爲什麼沒有可變參數，例如 add1 : Int -> Int
add1 x = x + 1
特別，我在twoPlusTwoNotFi
從類型驅動開發望着運動9.2與伊德里斯： data Last : List a -> a -> Type where
LastOne : Last [value] value
LastCons : (prf : Last xs value) -> Last (x :: xs) value
Uninhabited (Last [] value) where
unin
如果我有一個So的類型，比如So (x < y)，通過創造的東西像 IsLt : Ord a => (x: a) -> (y: a) -> Type
IsLt x y = So (x < y)
我怎樣才能提取(x < y)證明了這件事？我無法在標準庫中找到此功能。 So在標準庫中定義爲： data So : Bool -> Type where
Oh : So True
而且我
對於從屬類型，它可以定義一個感應式的有序列表，例如： data IsSorted : {a: Type} -> (ltRel: (a -> a -> Type)) -> List a -> Type where
IsSortedZero : IsSorted {a=a} ltRel Nil
IsSortedOne : (x: a) -> IsSorted ltRel [x]
我有一個Vehicle類型取決於PowerSource類型： data PowerSource = Petrol | Pedal | Electric
data Vehicle : PowerSource -> Type where
Unicycle : Vehicle Pedal
Motorcycle : (fuel: Nat) -> Vehicle Petrol