add search functions
This commit is contained in:
parent
28bc4568f7
commit
c7ac8bb7a7
@ -320,6 +320,28 @@ drop' SZ x = x
|
|||||||
drop' (SS n) (x :- xs) = drop' n xs
|
drop' (SS n) (x :- xs) = drop' n xs
|
||||||
|
|
||||||
|
|
||||||
|
-- * Searching vectors
|
||||||
|
-- Searching by equality
|
||||||
|
|
||||||
|
-- | Does the element occur in the structure?
|
||||||
|
elem ∷ Eq a ⇒ Vec a n → a → 𝔹
|
||||||
|
elem Nil _ = F
|
||||||
|
elem (x :- xs) y = (x ≡ y) ∨ (elem xs y)
|
||||||
|
|
||||||
|
|
||||||
|
-- | 'notElem' is the negation of 'elem'.
|
||||||
|
notElem ∷ Eq a ⇒ Vec a n → a → 𝔹
|
||||||
|
notElem xs = (¬) ∘ elem xs
|
||||||
|
|
||||||
|
|
||||||
|
-- | 'lookup' key assocs looks up a key in an association vector.
|
||||||
|
lookup ∷ Eq a ⇒ a → Vec (a, b) n → Maybe b
|
||||||
|
lookup t Nil = Nothing
|
||||||
|
lookup t ((k,v) :- x) =
|
||||||
|
if t ≡ k
|
||||||
|
then Just v
|
||||||
|
else lookup t x
|
||||||
|
|
||||||
|
|
||||||
-- * Zipping and unzipping vectors
|
-- * Zipping and unzipping vectors
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user