Libraries.Data.SnocList.Extra

Definitions

snocAppendFishAssociative : (sx : SnocList a) -> (sy : SnocList a) -> (zs : List a) -> (sx ++ sy) <>< zs = sx ++ (sy <>< zs)

Visibility: public export

snocAppendAsFish : (sx : SnocList a) -> (sy : SnocList a) -> sx ++ sy = sx <>< cast sy

Visibility: export

lookup : Eq a => a -> SnocList (a, b) -> Maybe b

Visibility: export

lengthDistributesOverFish : (sx : SnocList a) -> (ys : List a) -> length (sx <>< ys) = length sx + length ys

Visibility: export