1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 20:51:43 +03:00
Idris2/tests/idris2/interactive012/WithLift.idr
Edwin Brady a972778eab Add test script
They don't all pass yet, for minor reasons. Coming shortly...
Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 18:25:18 +01:00

28 lines
885 B
Idris

data Elem : a -> List a -> Type where
Here : Elem x (x :: xs)
There : Elem x xs -> Elem x (y :: xs)
interface DecEq a where
decEq : (x : a) -> (y : a) -> Dec (x = y)
zeroNotSucc : Z = (S k) -> Void
zeroNotSucc Refl impossible
recNotEq : (k = j -> Void) -> (S k) = (S j) -> Void
DecEq Nat where
decEq Z Z = Yes Refl
decEq Z (S k) = No zeroNotSucc
decEq (S k) Z = No ?succNotZero
decEq (S k) (S j) with (decEq k j)
decEq (S j) (S j) | (Yes Refl) = Yes Refl
decEq (S k) (S j) | (No contra) = No ?recNotEqLift
isElem : DecEq a => (x : a) -> (xs : List a) -> Maybe (Elem x xs)
isElem x [] = Nothing
isElem x (y :: xs) with (decEq x y)
isElem y (y :: xs) | (Yes Refl) = Just Here
isElem x (y :: xs) | (No contra) with (isElem x xs)
isElem x (y :: xs) | (No contra) | Nothing = Nothing
isElem x (y :: xs) | (No contra) | (Just z) = Just (There z)