mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-27 13:43:28 +03:00
a972778eab
They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
28 lines
929 B
Idris
28 lines
929 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)
|