Skip to content

Commit

Permalink
prelude's elem on Foldable suffices so remove SnocVect-specific imple…
Browse files Browse the repository at this point in the history
…mentation
  • Loading branch information
mattpolzin committed Jan 21, 2025
1 parent 19e5396 commit 3a7e0d0
Showing 1 changed file with 0 additions and 8 deletions.
8 changes: 0 additions & 8 deletions src/Data/SnocVect.idr
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,6 @@ module Data.SnocVect

import Data.Vect

%hide Prelude.Types.elem

%default total

||| A Backwards Vect
Expand Down Expand Up @@ -184,12 +182,6 @@ Traversable (SnocVect k) where
traverse _ Lin = pure Lin
traverse f (xs :< x) = [| traverse f xs :< f x |]

||| Check if something is a member of a snoc-vect using the default Boolean equality.
public export
elem : Eq a => a -> SnocVect k a -> Bool
elem x Lin = False
elem x (sx :< y) = x == y || elem x sx

||| Find the first element of the snoc-vect that satisfies the predicate.
public export
find : (a -> Bool) -> SnocVect k a -> Maybe a
Expand Down

0 comments on commit 3a7e0d0

Please sign in to comment.