Labelled sample

Conjectura.Defs.ComputerScience.Learning.LabelledSample

/-
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Samuel Schlesinger
-/
import Mathlib.Data.Fin.Basic

/-! # Labelled sample

## Source

Adapted for Conjectura from [cslib](https://github.com/leanprover/cslib), split into one concept per module. Released by its authors under Apache 2.0.
-/

namespace Conjectura.Learning

/-- A **labelled sample** of size `m` is a finite sequence of `(point, label)` pairs — the
training data a learner is given. -/
abbrev LabelledSample (α β : Type*) (m : ℕ) := Fin m → (α × β)

end Conjectura.Learning