Implementing isLast with Idris
Looking at Exercise 9.2 from type-driven development with Idris:
data Last : List a -> a -> Type where
LastOne : Last [value] value
LastCons : (prf : Last xs value) -> Last (x :: xs) value
Uninhabited (Last [] value) where
uninhabited LastOne impossible
uninhabited (LastCons _) impossible
notLast : Not (x = value) -> Last [x] value -> Void
notLast prf LastOne impossible
notLast prf (LastCons _) impossible
isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No absurd
isLast (x::[]) value = case decEq x value of
Yes Refl => Yes LastOne
No contra => No (notLast contra)
isLast (x::y::ys) value = ?rhs
I am getting compile time error in case notLast prf LastOne
:
*section1> :r
Type checking ./section1.idr
section1.idr:20:9:notLast prf LastOne is a valid case
Holes: Main.rhs, Main.notLast
Why does the compiler think this is a valid case?
+3
source to share
1 answer
Idris is not quite capable of seeing that he Not (value = value)
is isomorphic Void
, so you need to help him by explaining that the problem is like this:
notLast : Not (x = value) -> Last [x] value -> Void
notLast prf LastOne = absurd (prf Refl)
notLast prf (LastCons _) impossible
+4
source to share