Learner

Conjectura.Defs.ComputerScience.Learning.Learner

/-
Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Samuel Schlesinger
-/
import Conjectura.Defs.ComputerScience.Learning.LabelledSample

/-! # Learner

## 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 **learner** using `m` examples is a function turning a `LabelledSample` into a
hypothesis. Everything in learning theory is a statement about how well the output hypothesis
generalises beyond the sample. -/
abbrev Learner (α β : Type*) (m : ℕ) := LabelledSample α β m → (α → β)

end Conjectura.Learning