module FiniteSubsets.ListsWithDuplicates where open import IType.Bool open import IType.Nat open import IType.List open import FiniteSubsets.Interface member : Nat → List Nat → Bool member m [] = false member m (n :: ns) = eqNat m n || member m ns sizeFS : List Nat → Nat sizeFS [] = 0 sizeFS (n :: ns) = if member n ns then sizeFS ns else succ (sizeFS ns) ax-member-cons : (n : Nat) → (ns : List Nat) → So (member n (n :: ns)) ax-member-cons n ns = ||-intro (eqNat n n) (member n ns) (refleqNat n) ListsWithDuplicates : FiniteSubset ListsWithDuplicates = record { set = List Nat ; _∈_ = member ; size = sizeFS ; empty = [] ; insert = λ x s → x :: s ; ax-∈-insert = (λ {n} {ns} → ax-member-cons n ns) }