30 lines
757 B
Agda
30 lines
757 B
Agda
module Data.SnocList
|
|
|
|
import Prelude
|
|
|
|
snoclen : ∀ a. SnocList a → Nat
|
|
snoclen {a} xs = go xs Z
|
|
where
|
|
go : SnocList a → Nat → Nat
|
|
go Lin acc = acc
|
|
go (xs :< x) acc = go xs (S acc)
|
|
|
|
snoclen' : ∀ a. SnocList a → Int
|
|
snoclen' {a} xs = go xs 0
|
|
where
|
|
go : SnocList a → Int → Int
|
|
go Lin acc = acc
|
|
go (xs :< x) acc = go xs (1 + acc)
|
|
|
|
snocelem : ∀ a. {{Eq a}} → a → SnocList a → Bool
|
|
snocelem a Lin = False
|
|
snocelem a (xs :< x) = if a == x then True else snocelem a xs
|
|
|
|
snocGetAt : ∀ a. Nat → SnocList a → Maybe a
|
|
snocGetAt _ Lin = Nothing
|
|
snocGetAt Z (xs :< x) = Just x
|
|
snocGetAt (S k) (xs :< x) = snocGetAt k xs
|
|
|
|
snocGetAt' : ∀ a. Int → SnocList a → Maybe a
|
|
snocGetAt' ix xs = snocGetAt (cast ix) xs
|