Std.HashSet を使って リストから重複を取り除く例

import Std.Data.HashSet.Basic
/- # 投票アルゴリズム -/

/-- 投票結果 -/
def votes := ["Red", "Blue", "Green", "Blue", "Blue", "Red"]

/-- リストの中の特定の要素の数を数える -/
def count {α : Type} [BEq α] (x : α) (xs : List α) : Nat :=
  xs.filter (· == x) |>.length

#guard count 1 [1, 2, 3, 4, 1, 2, 3, 1, 2, 1] = 4

#guard count "Red" votes = 2

open Std (HashSet)

/-- リストから重複を削除する -/
def rmdups {α : Type} [BEq α] [Hashable α] (xs : List α) : List α :=
  HashSet.ofList xs |>.toList

#guard rmdups [1, 2, 3, 4, 1, 2, 3, 1, 2, 1] = [1, 2, 3, 4]

The issue provides a complete Lean example using Std.HashSet to remove duplicates from a list, but it does not name a documentation file or section. First inspect the repository's existing example structure and identify where this example belongs. Done means the example is added in the appropriate location and its #guard checks pass.