steshaw (13) [Avatar] Offline
#1
I've gotten stuck while implementing isLast. It looks like I'm almost there but perhaps I went wrong somewhere and need to back up? I'm still needing a solution for rhs but I only have two contradictions as arguments (which don't seem to provide much value):
data Last : List a -> a -> Type where
  LastOne  : Last [value] value
  LastCons : (prf : Last xs value) -> Last (x :: xs) value

last123 : Last [1, 2, 3] 3
last123 = LastCons (LastCons LastOne)

lastOnEmpty : Last [] value -> Void
lastOnEmpty LastOne impossible
lastOnEmpty (LastCons _) impossible

rhs : (contra2 : Last xs value -> Void) -> (contra1 : (xs = [value]) -> Void) -> Dec (Last (x :: xs) value)
rhs contra2 contra1 = ?rhs_rhs_2

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No lastOnEmpty
isLast (x :: xs) value = case decEq xs [value] of
                              Yes Refl => Yes (LastCons LastOne)
                              No contra1 => case isLast xs value of
                                                Yes prf => Yes (LastCons prf)
                                                No contra2 => rhs contra2 contra1