import Mathlib.Tactic
import Mathlib.Data.Finset.Basic

namespace Goppadecoding

section hamming

variable {k: Type _} [Field k] [DecidableEq k]
variable {U: Type _} [DecidableEq U]

def hamming_weight (α: U → k) (S: Finset U) :=
  (S.filter (fun s ↦ α s ≠ 0)).card

end hamming
