Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- data Last : List a -> a -> Type where
- LastOne : Last [val] val
- LastCons : (prf : Last xs val) -> Last (x :: xs) val
- Uninhabited (Last [] val) where
- uninhabited LastOne impossible
- uninhabited (LastCons _) impossible
- isLast : DecEq a => (xs : List a) -> (val : a) -> Dec (Last xs val)
- isLast [] val = No absurd
- isLast [x] val = case decEq x val of
- Yes Refl => Yes LastOne
- No contra => No (notLastOne contra)
- where
- notLastOne : (contra : (y = v) -> Void) -> Last [y] v -> Void
- notLastOne contra LastOne = contra Refl
- notLastOne contra (LastCons prf) = uninhabited prf
- isLast (x :: xs@(x' :: xs')) val = case isLast xs val of
- Yes prf => Yes (LastCons prf)
- No contra => No ?b -- (notLastCons contra)
- where
- notLastCons : (contra : Last ys v -> Void) -> Last (y :: ys) v -> Void
- {-
- - + Errors (1)
- `-- CheckEqDec.idr line 84 col 56:
- When checking right hand side of Main.case block in isLast at CheckEqDec.idr:83:41-53 with expected type
- Dec (Last (x :: x' :: xs') val)
- When checking argument prf to constructor Main.LastCons:
- Type mismatch between
- Last xs val (Type of prf)
- and
- Last (x' :: xs') val (Expected type)
- Specifically:
- Type mismatch between
- xs
- and
- x' :: xs'
- -}
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement